Let x0 of type ι be given.
Apply exp_SNo_nat_2 with
x0,
λ x1 x2 . SNoLe 0 x2 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply SNo_sqr_nonneg with
x0.
The subproof is completed by applying H0.
Apply SNo_sqrt_SNo_nonneg with
exp_SNo_nat x0 2 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
Apply sqrt_SNo_nonneg_nonneg with
exp_SNo_nat x0 2 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
Apply SNoLeE with
0,
x0,
sqrt_SNo_nonneg (exp_SNo_nat x0 2) = x0 leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply SNoLeE with
0,
sqrt_SNo_nonneg (exp_SNo_nat x0 2),
SNoLt 0 (sqrt_SNo_nonneg (exp_SNo_nat 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 L5.
The subproof is completed by applying H8.
Apply FalseE with
SNoLt 0 (sqrt_SNo_nonneg (exp_SNo_nat x0 2)).
Apply SNoLt_irref with
0.
Apply mul_SNo_zeroR with
0,
λ x1 x2 . SNoLt 0 x1 leaving 2 subgoals.
The subproof is completed by applying SNo_0.
Apply H8 with
λ x1 x2 . SNoLt 0 (mul_SNo x2 x2).
Apply L6 with
λ x1 x2 . SNoLt 0 x2.
Apply mul_SNo_pos_pos with
x0,
x0 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
The subproof is completed by applying H7.
The subproof is completed by applying H7.
Apply SNoLt_trichotomy_or_impred with
sqrt_SNo_nonneg (exp_SNo_nat x0 2),
x0,
sqrt_SNo_nonneg (exp_SNo_nat x0 2) = x0 leaving 5 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H0.
Apply FalseE with
sqrt_SNo_nonneg (exp_SNo_nat x0 2) = x0.
Apply SNoLt_irref with
mul_SNo x0 x0.
Apply L6 with
λ x1 x2 . SNoLt x1 (mul_SNo x0 x0).
Apply pos_mul_SNo_Lt2 with
sqrt_SNo_nonneg (exp_SNo_nat x0 2),
sqrt_SNo_nonneg (exp_SNo_nat x0 2),
x0,
x0 leaving 8 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L4.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
The subproof is completed by applying L8.
The subproof is completed by applying L8.
The subproof is completed by applying H9.
The subproof is completed by applying H9.
The subproof is completed by applying H9.
Apply FalseE with
sqrt_SNo_nonneg (exp_SNo_nat x0 2) = x0.
Apply SNoLt_irref with
mul_SNo x0 x0.
Apply L6 with
λ x1 x2 . SNoLt (mul_SNo x0 x0) x1.
Apply pos_mul_SNo_Lt2 with
x0,
x0,
sqrt_SNo_nonneg (exp_SNo_nat x0 2),
sqrt_SNo_nonneg (exp_SNo_nat x0 2) leaving 8 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
The subproof is completed by applying L4.
The subproof is completed by applying L4.
The subproof is completed by applying H7.
The subproof is completed by applying H7.
The subproof is completed by applying H9.
The subproof is completed by applying H9.
Assume H7: 0 = x0.
Apply exp_SNo_nat_2 with
x0,
λ x1 x2 . sqrt_SNo_nonneg x2 = x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply H7 with
λ x1 x2 . sqrt_SNo_nonneg (mul_SNo x1 x1) = x1.
Apply mul_SNo_zeroL with
0,
λ x1 x2 . sqrt_SNo_nonneg x2 = 0 leaving 2 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying sqrt_SNo_nonneg_0.