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 will
prove pa (proj0 z + proj0 (pa (- proj0 z) (- proj1 z))) (proj1 z + proj1 (pa (- proj0 z) (- proj1 z))) = 0.
rewrite the current goal using
CD_proj0_2 (- proj0 z) (- proj1 z) Lmp0z Lmp1z (from left to right).
rewrite the current goal using
CD_proj1_2 (- proj0 z) (- proj1 z) Lmp0z Lmp1z (from left to right).
rewrite the current goal using F_add_minus_rinv (proj0 z) Lp0z (from left to right).
rewrite the current goal using F_add_minus_rinv (proj1 z) Lp1z (from left to right).
We will prove pa 0 0 = 0.
An
exact proof term for the current goal is
pair_tag_0 0.