Let x be given.
Assume Hx Hxnonneg.
Set L_ to be the term λk ⇒ SNo_sqrtaux x sqrt_SNo_nonneg k 0 of type set → set.
Set R_ to be the term λk ⇒ SNo_sqrtaux x sqrt_SNo_nonneg k 1 of type set → set.
Set L to be the term ⋃k ∈ ωL_ k.
Set R to be the term ⋃k ∈ ωR_ k.
Assume H0: ∀k, nat_p k → (∀y ∈ L_ k, SNo y ∧ 0 ≤ y ∧ y * y < x) ∧ (∀y ∈ R_ k, SNo y ∧ 0 ≤ y ∧ x < y * y).
We will prove (∀x ∈ L, SNo x) ∧ (∀y ∈ R, SNo y) ∧ (∀x ∈ L, ∀y ∈ R, x < y).
Apply and3I to the current goal.
Let w be given.
Assume Hw: w ∈ L.
Apply famunionE_impred ω L_ w Hw to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H1: w ∈ L_ k.
Apply H0 k (omega_nat_p k Hk) to the current goal.
Assume H2 _.
Apply H2 w H1 to the current goal.
Assume H3 _.
Apply H3 to the current goal.
Assume H3 _.
An exact proof term for the current goal is H3.
Let z be given.
Assume Hz: z ∈ R.
Apply famunionE_impred ω R_ z Hz to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H1: z ∈ R_ k.
Apply H0 k (omega_nat_p k Hk) to the current goal.
Assume _ H2.
Apply H2 z H1 to the current goal.
Assume H3 _.
Apply H3 to the current goal.
Assume H3 _.
An exact proof term for the current goal is H3.
Let w be given.
Assume Hw: w ∈ L.
Let z be given.
Assume Hz: z ∈ R.
We will prove w < z.
Apply famunionE_impred ω L_ w Hw to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H1: w ∈ L_ k.
Apply H0 k (omega_nat_p k Hk) to the current goal.
Assume H2 _.
Apply H2 w H1 to the current goal.
Assume H.
Apply H to the current goal.
Assume Hw1: SNo w.
Assume Hw2: 0 ≤ w.
Assume Hw3: w * w < x.
Apply famunionE_impred ω R_ z Hz to the current goal.
Let k' be given.
Assume Hk': k' ∈ ω.
Assume H3: z ∈ R_ k'.
Apply H0 k' (omega_nat_p k' Hk') to the current goal.
Assume _ H4.
Apply H4 z H3 to the current goal.
Assume H.
Apply H to the current goal.
Assume Hz1: SNo z.
Assume Hz2: 0 ≤ z.
Assume Hz3: x < z * z.
We will prove w < z.
Apply SNoLtLe_or w z Hw1 Hz1 to the current goal.
Assume H5: w < z.
An exact proof term for the current goal is H5.
Assume H5: z ≤ w.
We will prove False.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
Apply SNoLt_tra x (z * z) x Hx (SNo_mul_SNo z z Hz1 Hz1) Hx Hz3 to the current goal.
We will prove z * z < x.
Apply SNoLeLt_tra (z * z) (w * w) x (SNo_mul_SNo z z Hz1 Hz1) (SNo_mul_SNo w w Hw1 Hw1) Hx to the current goal.
We will prove z * z ≤ w * w.
An exact proof term for the current goal is nonneg_mul_SNo_Le2 z z w w Hz1 Hz1 Hw1 Hw1 Hz2 Hz2 H5 H5.
An exact proof term for the current goal is Hw3.
∎