rewrite the current goal using mul_OSNo_mul_HSNo j j HSNo_Quaternion_j HSNo_Quaternion_j (from left to right).

rewrite the current goal using minus_OSNo_minus_HSNo 1 HSNo_1 (from left to right).

We will prove j * j = - 1.

An exact proof term for the current goal is Quaternion_j_sqr.

∎