Apply CSNo_ReIm_split (i ') (:-: i) (CSNo_conj_CSNo i CSNo_Complex_i) (CSNo_minus_CSNo i CSNo_Complex_i) to the current goal.
We will prove Re (i ') = Re (:-: i).
rewrite the current goal using conj_CSNo_CRe i CSNo_Complex_i (from left to right).
rewrite the current goal using minus_CSNo_CRe i CSNo_Complex_i (from left to right).
We will prove Re i = - Re i.
rewrite the current goal using Re_i (from left to right).
Use symmetry.
An exact proof term for the current goal is minus_SNo_0.
We will prove Im (i ') = Im (:-: i).
rewrite the current goal using minus_CSNo_CIm i CSNo_Complex_i (from left to right).
An exact proof term for the current goal is conj_CSNo_CIm i CSNo_Complex_i.
∎