rewrite the current goal using mul_OSNo_mul_HSNo k k HSNo_Quaternion_k HSNo_Quaternion_k (from left to right).

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

We will prove k * k = - 1.

An exact proof term for the current goal is Quaternion_k_sqr.

∎