Apply conj_HSNo_conj_CSNo with
Complex_i,
λ x0 x1 . x1 = minus_HSNo Complex_i leaving 2 subgoals.
The subproof is completed by applying CSNo_Complex_i.
Apply minus_HSNo_minus_CSNo with
Complex_i,
λ x0 x1 . conj_CSNo Complex_i = x1 leaving 2 subgoals.
The subproof is completed by applying CSNo_Complex_i.
The subproof is completed by applying conj_CSNo_i.