Let z and w be given.
Assume Hz Hw.
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 prove the intermediate claim Lmcp1z: F (- conj (proj1 z)).
Apply F_minus to the current goal.
An exact proof term for the current goal is Lcp1z.
We prove the intermediate claim Lmp1z: F (- proj1 z).
Apply F_minus to the current goal.
An exact proof term for the current goal is Lp1z.
We prove the intermediate claim Lp0w: F (proj0 w).
An exact proof term for the current goal is CD_proj0R w Hw.
We prove the intermediate claim Lp1w: F (proj1 w).
An exact proof term for the current goal is CD_proj1R w Hw.
We prove the intermediate claim Lcp0w: F (conj (proj0 w)).
Apply F_conj to the current goal.
An exact proof term for the current goal is Lp0w.
We prove the intermediate claim Lcp1w: F (conj (proj1 w)).
Apply F_conj to the current goal.
An exact proof term for the current goal is Lp1w.
We prove the intermediate claim Lmp1w: F (- proj1 w).
Apply F_minus to the current goal.
An exact proof term for the current goal is Lp1w.
We prove the intermediate claim Lp0zp0w: F (proj0 z * proj0 w).
Apply F_mul to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lcp1wp1z: F (conj (proj1 w) * proj1 z).
Apply F_mul to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lcp1wp1z: F (- conj (proj1 w) * proj1 z).
Apply F_minus to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim LzwL: F (proj0 z * proj0 w + - conj (proj1 w) * proj1 z).
Apply F_add to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lp1wp0z: F (proj1 w * proj0 z).
Apply F_mul to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lp1zcp0w: F (proj1 z * conj (proj0 w)).
Apply F_mul to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim LzwR: F (proj1 w * proj0 z + proj1 z * conj (proj0 w)).
Apply F_add to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Set w' to be the term pa (conj (proj0 w)) (- proj1 w).
Set z' to be the term pa (conj (proj0 z)) (- proj1 z).
We prove the intermediate claim Lp0w': F (proj0 w').
An exact proof term for the current goal is CD_proj0R (CD_conj minus conj w) (CD_conj_CD minus F_minus conj F_conj w Hw).
We prove the intermediate claim Lp1w': F (proj1 w').
An exact proof term for the current goal is CD_proj1R (CD_conj minus conj w) (CD_conj_CD minus F_minus conj F_conj w Hw).
We prove the intermediate claim Lp0z': F (proj0 z').
An exact proof term for the current goal is CD_proj0R (CD_conj minus conj z) (CD_conj_CD minus F_minus conj F_conj z Hz).
We prove the intermediate claim Lp1z': F (proj1 z').
An exact proof term for the current goal is CD_proj1R (CD_conj minus conj z) (CD_conj_CD minus F_minus conj F_conj 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 ??.
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 ??.
We prove the intermediate claim Lp0w'p0z': F (proj0 w' * proj0 z').
Apply F_mul to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lcp1z'p1w': F (conj (proj1 z') * proj1 w').
Apply F_mul to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lcp1z'p1w': F (- conj (proj1 z') * proj1 w').
Apply F_minus to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lw'z'L: F (proj0 w' * proj0 z' + - conj (proj1 z') * proj1 w').
Apply F_add to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lp1z'p0w': F (proj1 z' * proj0 w').
Apply F_mul to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lp1w'cp0z': F (proj1 w' * conj (proj0 z')).
Apply F_mul to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lw'z'R: F (proj1 z' * proj0 w' + proj1 w' * conj (proj0 z')).
Apply F_add to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lcp1zp1w: F (conj (proj1 z) * proj1 w).
Apply F_mul to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lmp1zcp0w: F ((- proj1 z) * (conj (proj0 w))).
Apply F_mul to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim Lmp1wp0z: F ((- proj1 w) * proj0 z).
Apply F_mul to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We will prove pa (conj (proj0 (pa (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w))))) (- (proj1 (pa (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w))))) = pa (proj0 w' * proj0 z' + - conj (proj1 z') * proj1 w') (proj1 z' * proj0 w' + proj1 w' * conj (proj0 z')).
rewrite the current goal using CD_proj0_2 (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)) ?? ?? (from left to right).
rewrite the current goal using CD_proj1_2 (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)) ?? ?? (from left to right).
We will prove pa (conj (proj0 z * proj0 w + - conj (proj1 w) * proj1 z)) (- (proj1 w * proj0 z + proj1 z * conj (proj0 w))) = pa (proj0 w' * proj0 z' + - conj (proj1 z') * proj1 w') (proj1 z' * proj0 w' + proj1 w' * conj (proj0 z')).
rewrite the current goal using CD_proj0_2 (conj (proj0 w)) (- proj1 w) ?? ?? (from left to right).
rewrite the current goal using CD_proj1_2 (conj (proj0 w)) (- proj1 w) ?? ?? (from left to right).
rewrite the current goal using CD_proj0_2 (conj (proj0 z)) (- proj1 z) ?? ?? (from left to right).
rewrite the current goal using CD_proj1_2 (conj (proj0 z)) (- proj1 z) ?? ?? (from left to right).
We will prove pa (conj (proj0 z * proj0 w + - conj (proj1 w) * proj1 z)) (- (proj1 w * proj0 z + proj1 z * conj (proj0 w))) = pa (conj (proj0 w) * conj (proj0 z) + - conj (- proj1 z) * (- proj1 w)) ((- proj1 z) * (conj (proj0 w)) + (- proj1 w) * conj (conj (proj0 z))).
Use f_equal.
We will prove conj (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) = conj (proj0 w) * conj (proj0 z) + - conj (- proj1 z) * (- proj1 w).
rewrite the current goal using F_conj_add (proj0 z * proj0 w) (- conj (proj1 w) * proj1 z) ?? ?? (from left to right).
We will prove conj (proj0 z * proj0 w) + conj (- conj (proj1 w) * proj1 z) = conj (proj0 w) * conj (proj0 z) + - conj (- proj1 z) * (- proj1 w).
Use f_equal.
We will prove conj (proj0 z * proj0 w) = conj (proj0 w) * conj (proj0 z).
An exact proof term for the current goal is F_conj_mul (proj0 z) (proj0 w) ?? ??.
We will prove conj (- conj (proj1 w) * proj1 z) = - conj (- proj1 z) * (- proj1 w).
rewrite the current goal using F_conj_minus (conj (proj1 w) * proj1 z) ?? (from left to right).
Use f_equal.
We will prove conj (conj (proj1 w) * proj1 z) = conj (- proj1 z) * (- proj1 w).
rewrite the current goal using F_conj_mul (conj (proj1 w)) (proj1 z) ?? ?? (from left to right).
We will prove conj (proj1 z) * (conj (conj (proj1 w))) = conj (- proj1 z) * (- proj1 w).
rewrite the current goal using F_conj_invol (proj1 w) ?? (from left to right).
We will prove conj (proj1 z) * proj1 w = conj (- proj1 z) * (- proj1 w).
rewrite the current goal using F_conj_minus (proj1 z) ?? (from left to right).
We will prove conj (proj1 z) * proj1 w = (- conj (proj1 z)) * (- proj1 w).
rewrite the current goal using F_minus_mul_distrR (- conj (proj1 z)) (proj1 w) ?? ?? (from left to right).
rewrite the current goal using F_minus_mul_distrL (conj (proj1 z)) (proj1 w) ?? ?? (from left to right).
Use symmetry.
Apply F_minus_invol (conj (proj1 z) * proj1 w) ?? to the current goal.
We will prove - (proj1 w * proj0 z + proj1 z * conj (proj0 w)) = (- proj1 z) * (conj (proj0 w)) + (- proj1 w) * conj (conj (proj0 z)).
rewrite the current goal using F_conj_invol (proj0 z) ?? (from left to right).
rewrite the current goal using F_minus_add (proj1 w * proj0 z) (proj1 z * conj (proj0 w)) ?? ?? (from left to right).
rewrite the current goal using F_add_com ((- proj1 z) * (conj (proj0 w))) ((- proj1 w) * proj0 z) ?? ?? (from left to right).
Use f_equal.
We will prove - proj1 w * proj0 z = (- proj1 w) * proj0 z.
Use symmetry.
An exact proof term for the current goal is F_minus_mul_distrL (proj1 w) (proj0 z) ?? ??.
We will prove - proj1 z * conj (proj0 w) = (- proj1 z) * (conj (proj0 w)).
Use symmetry.
An exact proof term for the current goal is F_minus_mul_distrL (proj1 z) (conj (proj0 w)) ?? ??.
∎