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 will
prove pa (proj0 z * proj0 0 + - conj (proj1 0) * proj1 z) (proj1 0 * proj0 z + proj1 z * conj (proj0 0)) = 0.
rewrite the current goal using
CD_proj0_F F_0 0 F_0 (from left to right).
rewrite the current goal using
CD_proj1_F F_0 0 F_0 (from left to right).
We will
prove pa (proj0 z * 0 + - conj 0 * proj1 z) (0 * proj0 z + proj1 z * conj 0) = 0.
rewrite the current goal using F_conj_0 (from left to right).
We will
prove pa (proj0 z * 0 + - 0 * proj1 z) (0 * proj0 z + proj1 z * 0) = 0.
rewrite the current goal using F_mul_0L (proj0 z) ?? (from left to right).
rewrite the current goal using F_mul_0L (proj1 z) ?? (from left to right).
rewrite the current goal using F_mul_0R (proj0 z) ?? (from left to right).
rewrite the current goal using F_mul_0R (proj1 z) ?? (from left to right).
rewrite the current goal using F_minus_0 (from left to right).
We will
prove pa (0 + 0) (0 + 0) = 0.
rewrite the current goal using F_add_0_0 (from left to right).
We will prove pa 0 0 = 0.
An
exact proof term for the current goal is
pair_tag_0 0.