rewrite the current goal using mul_HSNo_mul_CSNo i i CSNo_Complex_i CSNo_Complex_i (from left to right).

rewrite the current goal using minus_HSNo_minus_CSNo 1 CSNo_1 (from left to right).

We will prove i * i = - 1.

An exact proof term for the current goal is Complex_i_sqr.

∎