Let z and w be given.
Assume Hz Hw.
We will prove CD_carr (pa (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w))).
Apply CD_carr_I to the current goal.
Apply F_add to the current goal.
Apply F_mul to the current goal.
Apply CD_proj0R to the current goal.
An exact proof term for the current goal is Hz.
Apply CD_proj0R to the current goal.
An exact proof term for the current goal is Hw.
Apply F_minus to the current goal.
Apply F_mul to the current goal.
Apply F_conj to the current goal.
Apply CD_proj1R to the current goal.
An exact proof term for the current goal is Hw.
Apply CD_proj1R to the current goal.
An exact proof term for the current goal is Hz.
Apply F_add to the current goal.
Apply F_mul to the current goal.
Apply CD_proj1R to the current goal.
An exact proof term for the current goal is Hw.
Apply CD_proj0R to the current goal.
An exact proof term for the current goal is Hz.
Apply F_mul to the current goal.
Apply CD_proj1R to the current goal.
An exact proof term for the current goal is Hz.
Apply F_conj to the current goal.
Apply CD_proj0R to the current goal.
An exact proof term for the current goal is Hw.
∎