Let x0 of type ι be given.
Apply CSNo_ReR with
x0.
The subproof is completed by applying H0.
Apply CSNo_ImR with
x0.
The subproof is completed by applying H0.
Apply SNo_exp_SNo_nat with
CSNo_Re x0,
2 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying nat_2.
Apply SNo_exp_SNo_nat with
CSNo_Im x0,
2 leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying nat_2.
Apply SNo_add_SNo with
exp_SNo_nat (CSNo_Re x0) 2,
exp_SNo_nat (CSNo_Im x0) 2 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
Apply CSNo_ReIm_split with
x0,
0 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying CSNo_0.
Apply Re_0 with
λ x1 x2 . CSNo_Re x0 = x2.
Apply SNo_zero_or_sqr_pos' with
CSNo_Re x0,
CSNo_Re x0 = 0 leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H7.
Apply FalseE with
CSNo_Re x0 = 0.
Apply SNoLt_irref with
0.
Apply H1 with
λ x1 x2 . SNoLt 0 x1.
Apply SNoLtLe_tra with
0,
exp_SNo_nat (CSNo_Re x0) 2,
add_SNo (exp_SNo_nat (CSNo_Re x0) 2) (exp_SNo_nat (CSNo_Im x0) 2) leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L4.
The subproof is completed by applying L6.
The subproof is completed by applying H7.
Apply Im_0 with
λ x1 x2 . CSNo_Im x0 = x2.
Apply SNo_zero_or_sqr_pos' with
CSNo_Im x0,
CSNo_Im x0 = 0 leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying H7.
Apply FalseE with
CSNo_Im x0 = 0.
Apply SNoLt_irref with
0.
Apply H1 with
λ x1 x2 . SNoLt 0 x1.
Apply SNoLtLe_tra with
0,
exp_SNo_nat (CSNo_Im x0) 2,
add_SNo (exp_SNo_nat (CSNo_Re x0) 2) (exp_SNo_nat (CSNo_Im x0) 2) leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L5.
The subproof is completed by applying L6.
The subproof is completed by applying H7.