Let z be given.
Assume Hz.
We prove the intermediate claim Lp0z: F (proj0 z).
An
exact proof term for the current goal is
CD_proj0R z Hz.
We prove the intermediate claim Lp1z: F (proj1 z).
An
exact proof term for the current goal is
CD_proj1R z Hz.
We prove the intermediate claim Lcp0z: F (conj (proj0 z)).
Apply F_conj to the current goal.
An exact proof term for the current goal is Lp0z.
We prove the intermediate claim Lcp1z: F (conj (proj1 z)).
Apply F_conj to the current goal.
An exact proof term for the current goal is Lp1z.
We will
prove pa (proj0 1 * proj0 z + - conj (proj1 z) * proj1 1) (proj1 z * proj0 1 + proj1 1 * conj (proj0 z)) = z.
rewrite the current goal using
CD_proj0_F F_0 1 F_1 (from left to right).
rewrite the current goal using
CD_proj1_F F_0 1 F_1 (from left to right).
We will
prove pa (1 * proj0 z + - conj (proj1 z) * 0) (proj1 z * 1 + 0 * conj (proj0 z)) = z.
rewrite the current goal using F_mul_1L (proj0 z) ?? (from left to right).
rewrite the current goal using F_mul_1R (proj1 z) ?? (from left to right).
rewrite the current goal using F_mul_0L (conj (proj0 z)) ?? (from left to right).
rewrite the current goal using F_mul_0R (conj (proj1 z)) ?? (from left to right).
We will
prove pa (proj0 z + - 0) (proj1 z + 0) = z.
rewrite the current goal using F_minus_0 (from left to right).
rewrite the current goal using F_add_0R (proj0 z) ?? (from left to right).
rewrite the current goal using F_add_0R (proj1 z) ?? (from left to right).
We will prove pa (proj0 z) (proj1 z) = z.
Use symmetry.
∎