Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNo x1.
Assume H2: SNoLe 0 x0.
Assume H3: SNoLt x0 x1.
Claim L4: SNo (sqrt_SNo_nonneg x0)
Apply SNo_sqrt_SNo_nonneg with x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Claim L5: SNoLe 0 (sqrt_SNo_nonneg x0)
Apply sqrt_SNo_nonneg_nonneg with x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Claim L6: SNoLe 0 x1
Apply SNoLe_tra with 0, x0, x1 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.
The subproof is completed by applying H2.
Apply SNoLtLe with x0, x1.
The subproof is completed by applying H3.
Claim L7: SNo (sqrt_SNo_nonneg x1)
Apply SNo_sqrt_SNo_nonneg with x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying L6.
Claim L8: SNoLe 0 (sqrt_SNo_nonneg x1)
Apply sqrt_SNo_nonneg_nonneg with x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying L6.
Apply SNoLtLe_or with sqrt_SNo_nonneg x0, sqrt_SNo_nonneg x1, SNoLt (sqrt_SNo_nonneg x0) (sqrt_SNo_nonneg x1) leaving 4 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L7.
Assume H9: SNoLt (sqrt_SNo_nonneg x0) (sqrt_SNo_nonneg x1).
The subproof is completed by applying H9.
Assume H9: SNoLe (sqrt_SNo_nonneg x1) (sqrt_SNo_nonneg x0).
Apply FalseE with SNoLt (sqrt_SNo_nonneg x0) (sqrt_SNo_nonneg x1).
Apply SNoLt_irref with x0.
Apply SNoLtLe_tra with x0, x1, x0 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Apply sqrt_SNo_nonneg_sqr with x1, λ x2 x3 . SNoLe x2 x0 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying L6.
Apply sqrt_SNo_nonneg_sqr with x0, λ x2 x3 . SNoLe (mul_SNo (sqrt_SNo_nonneg x1) (sqrt_SNo_nonneg x1)) x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply nonneg_mul_SNo_Le2 with sqrt_SNo_nonneg x1, sqrt_SNo_nonneg x1, sqrt_SNo_nonneg x0, sqrt_SNo_nonneg x0 leaving 8 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L7.
The subproof is completed by applying L4.
The subproof is completed by applying L4.
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.
■