We prove the intermediate claim Lii: CSNo (i ⨯ i).
An exact proof term for the current goal is CSNo_mul_CSNo i i CSNo_Complex_i CSNo_Complex_i.
We prove the intermediate claim Lm1: CSNo (:-: 1).
An exact proof term for the current goal is CSNo_minus_CSNo 1 CSNo_1.
Apply CSNo_ReIm_split (i ⨯ i) (:-: 1) Lii Lm1 to the current goal.
We will prove Re (i ⨯ i) = Re (:-: 1).
rewrite the current goal using mul_CSNo_CRe i i CSNo_Complex_i CSNo_Complex_i (from left to right).
rewrite the current goal using minus_CSNo_CRe 1 CSNo_1 (from left to right).
We will prove Re i * Re i + - Im i * Im i = - Re 1.
rewrite the current goal using Re_i (from left to right).
rewrite the current goal using Im_i (from left to right).
rewrite the current goal using Re_1 (from left to right).
We will prove 0 * 0 + - 1 * 1 = - 1.
rewrite the current goal using mul_SNo_zeroL 0 SNo_0 (from left to right).
rewrite the current goal using mul_SNo_oneL 1 SNo_1 (from left to right).
We will prove 0 + - 1 = - 1.
An exact proof term for the current goal is add_SNo_0L (- 1) (SNo_minus_SNo 1 SNo_1).
We will prove Im (i ⨯ i) = Im (:-: 1).
rewrite the current goal using mul_CSNo_CIm i i CSNo_Complex_i CSNo_Complex_i (from left to right).
rewrite the current goal using minus_CSNo_CIm 1 CSNo_1 (from left to right).
We will prove Im i * Re i + Im i * Re i = - Im 1.
rewrite the current goal using Re_i (from left to right).
rewrite the current goal using Im_i (from left to right).
rewrite the current goal using Im_1 (from left to right).
We will prove 1 * 0 + 1 * 0 = - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
rewrite the current goal using mul_SNo_zeroR 1 SNo_1 (from left to right).
We will prove 0 + 0 = 0.
An exact proof term for the current goal is add_SNo_0L 0 SNo_0.
∎