Apply mul_HSNo_mul_CSNo with
Complex_i,
Complex_i,
λ x0 x1 . x1 = minus_HSNo 1 leaving 3 subgoals.
The subproof is completed by applying CSNo_Complex_i.
The subproof is completed by applying CSNo_Complex_i.
Apply minus_HSNo_minus_CSNo with
1,
λ x0 x1 . mul_CSNo Complex_i Complex_i = x1 leaving 2 subgoals.
The subproof is completed by applying CSNo_1.
The subproof is completed by applying Complex_i_sqr.