Let x0 of type ι be given.

Assume H0: SNo x0.

Assume H1: SNoLe 0 x0.

Let x1 of type ι be given.

Assume H2: nat_p x1.

Apply SNo_sqrtaux_0_1_prop with x0, x1, ∀ x2 . x2 ∈ ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0 ⟶ and (and (SNo x2) (SNoLe 0 x2)) (SNoLt (mul_SNo x2 x2) x0) leaving 4 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

Assume H3: ∀ x2 . x2 ∈ ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0 ⟶ and (and (SNo x2) (SNoLe 0 x2)) (SNoLt (mul_SNo x2 x2) x0).

Assume H4: ∀ x2 . x2 ∈ ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1 ⟶ and (and (SNo x2) (SNoLe 0 x2)) (SNoLt x0 (mul_SNo x2 x2)).

The subproof is completed by applying H3.

■

Proofgold Proof