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 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 Lmp0z:
F (- proj0 z).
Apply F_minus to the current goal.
An exact proof term for the current goal is ??.
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 ??.
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 ??.
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 ??.
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 Lmcp1wp1z:
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 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 LmulL:
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 LmulR:
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 ??.
We will
prove pa (proj0 (pa (- proj0 z) (- proj1 z)) * proj0 w + - conj (proj1 w) * proj1 (pa (- proj0 z) (- proj1 z))) (proj1 w * proj0 (pa (- proj0 z) (- proj1 z)) + proj1 (pa (- proj0 z) (- proj1 z)) * conj (proj0 w)) = pa (- 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)))).
rewrite the current goal using
CD_proj0_2 (- proj0 z) (- proj1 z) ?? ?? (from left to right).
rewrite the current goal using
CD_proj1_2 (- proj0 z) (- proj1 z) ?? ?? (from left to right).
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 ((- proj0 z) * proj0 w + - conj (proj1 w) * (- proj1 z)) (proj1 w * (- proj0 z) + (- proj1 z) * conj (proj0 w)) = pa (- (proj0 z * proj0 w + - conj (proj1 w) * proj1 z)) (- (proj1 w * proj0 z + proj1 z * conj (proj0 w))).
Use f_equal.
We will
prove (- proj0 z) * proj0 w + - conj (proj1 w) * (- proj1 z) = - (proj0 z * proj0 w + - conj (proj1 w) * proj1 z).
rewrite the current goal using
F_minus_add (proj0 z * proj0 w) (- conj (proj1 w) * proj1 z) ?? ?? (from left to right).
Use f_equal.
We will
prove (- proj0 z) * proj0 w = - proj0 z * proj0 w.
An exact proof term for the current goal is F_minus_mul_distrL (proj0 z) (proj0 w) ?? ??.
We will
prove - conj (proj1 w) * (- proj1 z) = - - conj (proj1 w) * proj1 z.
Use f_equal.
We will
prove conj (proj1 w) * (- proj1 z) = - conj (proj1 w) * proj1 z.
An exact proof term for the current goal is F_minus_mul_distrR (conj (proj1 w)) (proj1 z) ?? ??.
We will
prove proj1 w * (- proj0 z) + (- proj1 z) * conj (proj0 w) = - (proj1 w * proj0 z + proj1 z * conj (proj0 w)).
rewrite the current goal using
F_minus_add (proj1 w * proj0 z) (proj1 z * conj (proj0 w)) ?? ?? (from left to right).
Use f_equal.
We will
prove proj1 w * (- proj0 z) = - proj1 w * proj0 z.
An exact proof term for the current goal is F_minus_mul_distrR (proj1 w) (proj0 z) ?? ??.
We will
prove (- proj1 z) * conj (proj0 w) = - proj1 z * conj (proj0 w).
An exact proof term for the current goal is F_minus_mul_distrL (proj1 z) (conj (proj0 w)) ?? ??.