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 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 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 Lp0zw:
F (proj0 z + 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 prove the intermediate
claim Lp1zw:
F (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 will
prove pa (conj (proj0 (pa (proj0 z + proj0 w) (proj1 z + proj1 w)))) (- proj1 (pa (proj0 z + proj0 w) (proj1 z + proj1 w))) = pa (proj0 (pa (conj (proj0 z)) (- proj1 z)) + proj0 (pa (conj (proj0 w)) (- proj1 w))) (proj1 (pa (conj (proj0 z)) (- proj1 z)) + proj1 (pa (conj (proj0 w)) (- proj1 w))).
rewrite the current goal using
CD_proj0_2 (proj0 z + proj0 w) (proj1 z + proj1 w) ?? ?? (from left to right).
rewrite the current goal using
CD_proj1_2 (proj0 z + proj0 w) (proj1 z + proj1 w) ?? ?? (from left to right).
rewrite the current goal using
CD_proj0_2 (conj (proj0 z)) (- proj1 z) Lcp0z Lmp1z (from left to right).
rewrite the current goal using
CD_proj1_2 (conj (proj0 z)) (- proj1 z) Lcp0z Lmp1z (from left to right).
rewrite the current goal using
CD_proj0_2 (conj (proj0 w)) (- proj1 w) Lcp0w Lmp1w (from left to right).
rewrite the current goal using
CD_proj1_2 (conj (proj0 w)) (- proj1 w) Lcp0w Lmp1w (from left to right).
Use f_equal.
Apply F_conj_add to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply F_minus_add to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.