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

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

We will prove i ' = - i.

An exact proof term for the current goal is conj_CSNo_i.

∎