rewrite the current goal using mul_OSNo_mul_HSNo i i HSNo_Complex_i HSNo_Complex_i (from left to right).

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

We will prove i * i = - 1.

An exact proof term for the current goal is Quaternion_i_sqr.

∎