Let x0 of type ι be given.
Apply quaternion_I with
conj_CSNo (HSNo_proj0 x0),
minus_CSNo (HSNo_proj1 x0) leaving 2 subgoals.
Apply complex_conj_CSNo with
HSNo_proj0 x0.
Apply quaternion_p0_complex with
x0.
The subproof is completed by applying H0.
Apply complex_minus_CSNo with
HSNo_proj1 x0.
Apply quaternion_p1_complex with
x0.
The subproof is completed by applying H0.