Let x and y be given.

Assume Hx Hy.

We will prove pa (proj0 x * proj0 y + - conj (proj1 y) * proj1 x) (proj1 y * proj0 x + proj1 x * conj (proj0 y)) = x * y.

rewrite the current goal using CD_proj0_F F_0 x Hx (from left to right).

rewrite the current goal using CD_proj1_F F_0 x Hx (from left to right).

rewrite the current goal using CD_proj0_F F_0 y Hy (from left to right).

rewrite the current goal using CD_proj1_F F_0 y Hy (from left to right).

We will prove pa (x * y + - conj 0 * 0) (0 * x + 0 * conj y) = x * y.

rewrite the current goal using F_mul_0R (conj 0) (F_conj 0 F_0) (from left to right).

rewrite the current goal using F_mul_0L x Hx (from left to right).

rewrite the current goal using F_mul_0L (conj y) (F_conj y Hy) (from left to right).

rewrite the current goal using F_minus_0 (from left to right).

rewrite the current goal using F_add_0R 0 F_0 (from left to right).

rewrite the current goal using F_add_0R (x * y) (F_mul x y Hx Hy) (from left to right).

We will prove pa (x * y) 0 = x * y.

An exact proof term for the current goal is pair_tag_0 (x * y).

∎