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 Lmp0z:
F (- proj0 z).
Apply F_minus to the current goal.
An exact proof term for the current goal is Lp0z.
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 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 Lcmp0z:
F (conj (- proj0 z)).
Apply F_conj to the current goal.
An exact proof term for the current goal is Lmp0z.
We will
prove pa (conj (proj0 (pa (- (proj0 z)) (- (proj1 z))))) (- proj1 (pa (- (proj0 z)) (- (proj1 z)))) = pa (- proj0 (pa (conj (proj0 z)) (- proj1 z))) (- proj1 (pa (conj (proj0 z)) (- proj1 z))).
Use f_equal.
We will
prove conj (proj0 (pa (- (proj0 z)) (- (proj1 z)))) = - proj0 (pa (conj (proj0 z)) (- proj1 z)).
rewrite the current goal using
CD_proj0_2 (- proj0 z) (- proj1 z) ?? ?? (from left to right).
rewrite the current goal using
CD_proj0_2 (conj (proj0 z)) (- proj1 z) ?? ?? (from left to right).
We will
prove conj (- proj0 z) = - conj (proj0 z).
An exact proof term for the current goal is F_conj_minus (proj0 z) ??.
We will
prove - proj1 (pa (- (proj0 z)) (- (proj1 z))) = - proj1 (pa (conj (proj0 z)) (- proj1 z)).
Use f_equal.
rewrite the current goal using
CD_proj1_2 (conj (proj0 z)) (- (proj1 z)) ?? ?? (from left to right).
An
exact proof term for the current goal is
CD_proj1_2 (- (proj0 z)) (- (proj1 z)) ?? ??.