Let x be given.

Assume Hx.

rewrite the current goal using HSNo_pair_0 x (from right to left) at position 1.

An exact proof term for the current goal is octonion_p0_eq x Hx 0 quaternion_0.

∎