Let z be given.

Assume Hz.

We will prove pa (conj_CSNo (p0 z)) (minus_CSNo (p1 z)) ∈ quaternion.

Apply quaternion_I to the current goal.

Apply complex_conj_CSNo to the current goal.

An exact proof term for the current goal is quaternion_p0_complex z Hz.

Apply complex_minus_CSNo to the current goal.

An exact proof term for the current goal is quaternion_p1_complex z Hz.

∎