Apply CSNo_ReIm_split with
conj_CSNo Complex_i,
minus_CSNo Complex_i leaving 4 subgoals.
Apply CSNo_conj_CSNo with
Complex_i.
The subproof is completed by applying CSNo_Complex_i.
Apply CSNo_minus_CSNo with
Complex_i.
The subproof is completed by applying CSNo_Complex_i.
Apply conj_CSNo_CRe with
Complex_i,
λ x0 x1 . x1 = CSNo_Re (minus_CSNo Complex_i) leaving 2 subgoals.
The subproof is completed by applying CSNo_Complex_i.
Apply minus_CSNo_CRe with
Complex_i,
λ x0 x1 . CSNo_Re Complex_i = x1 leaving 2 subgoals.
The subproof is completed by applying CSNo_Complex_i.
Apply Re_i with
λ x0 x1 . x1 = minus_SNo x1.
Let x0 of type ι → ι → ο be given.
The subproof is completed by applying minus_SNo_0 with λ x1 x2 . x0 x2 x1.
Apply minus_CSNo_CIm with
Complex_i,
λ x0 x1 . CSNo_Im (conj_CSNo Complex_i) = x1 leaving 2 subgoals.
The subproof is completed by applying CSNo_Complex_i.
Apply conj_CSNo_CIm with
Complex_i.
The subproof is completed by applying CSNo_Complex_i.