Let x0 of type ι be given.
Let x1 of type ι be given.
Apply SNo_sqrt_SNo_nonneg with
x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply sqrt_SNo_nonneg_nonneg with
x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply SNo_sqrt_SNo_nonneg with
x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Apply sqrt_SNo_nonneg_nonneg with
x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Apply SNo_mul_SNo with
sqrt_SNo_nonneg x0,
sqrt_SNo_nonneg x1 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L6.
Apply exp_SNo_nat_2 with
mul_SNo (sqrt_SNo_nonneg x0) (sqrt_SNo_nonneg x1),
λ x2 x3 . x3 = mul_SNo x0 x1 leaving 2 subgoals.
The subproof is completed by applying L8.
Apply mul_SNo_com_4_inner_mid with
sqrt_SNo_nonneg x0,
sqrt_SNo_nonneg x1,
sqrt_SNo_nonneg x0,
sqrt_SNo_nonneg x1,
λ x2 x3 . x3 = mul_SNo x0 x1 leaving 5 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L6.
The subproof is completed by applying L4.
The subproof is completed by applying L6.
Claim L9: ∀ x4 : ι → ο . x4 y3 ⟶ x4 y2
Let x4 of type ι → ο be given.
set y5 to be λ x5 . x4
Apply sqrt_SNo_nonneg_sqr with
y2,
λ x6 x7 . y5 (mul_SNo x6 (mul_SNo (sqrt_SNo_nonneg y3) (sqrt_SNo_nonneg y3))) (mul_SNo x7 (mul_SNo (sqrt_SNo_nonneg y3) (sqrt_SNo_nonneg y3))) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
set y6 to be λ x6 . y5
Apply sqrt_SNo_nonneg_sqr with
x4,
λ x7 x8 . y6 (mul_SNo y3 x7) (mul_SNo y3 x8) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H9.
Let x4 of type ι → ι → ο be given.
Apply L9 with
λ x5 . x4 x5 y3 ⟶ x4 y3 x5.
Assume H10: x4 y3 y3.
The subproof is completed by applying H10.