Let x be given.

Assume Hx.

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

An exact proof term for the current goal is quaternion_p1_eq x Hx 0 complex_0.

∎