Apply SNoLev_ind to the current goal.
Let x be given.
Assume Hx: SNo x.
Assume IH: ∀w ∈ SNoS_ (SNoLev x), 0 ≤ w → SNo (sqrt_SNo_nonneg w) ∧ 0 ≤ sqrt_SNo_nonneg w ∧ sqrt_SNo_nonneg w * sqrt_SNo_nonneg w = w.
Assume Hxnonneg: 0 ≤ x.
We will prove SNo (sqrt_SNo_nonneg x) ∧ 0 ≤ sqrt_SNo_nonneg x ∧ sqrt_SNo_nonneg x * sqrt_SNo_nonneg x = x.
rewrite the current goal using sqrt_SNo_nonneg_eq x Hx (from left to right).
We will prove SNo (G x sqrt_SNo_nonneg) ∧ 0 ≤ G x sqrt_SNo_nonneg ∧ G x sqrt_SNo_nonneg * G x sqrt_SNo_nonneg = x.
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.
We prove the intermediate claim LL_mon: ∀k k', nat_p k → nat_p k' → k ⊆ k' → L_ k ⊆ L_ k'.
Let k and k' be given.
Assume Hk Hk' Hkk'.
Apply SNo_sqrtaux_mon x sqrt_SNo_nonneg k Hk k' Hk' Hkk' to the current goal.
Assume H _.
An exact proof term for the current goal is H.
We prove the intermediate claim LR_mon: ∀k k', nat_p k → nat_p k' → k ⊆ k' → R_ k ⊆ R_ k'.
Let k and k' be given.
Assume Hk Hk' Hkk'.
Apply SNo_sqrtaux_mon x sqrt_SNo_nonneg k Hk k' Hk' Hkk' to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
We prove the intermediate claim L1: ∀k, nat_p k → (∀y ∈ L_ k, SNo y ∧ 0 ≤ y ∧ y * y < x) ∧ (∀y ∈ R_ k, SNo y ∧ 0 ≤ y ∧ x < y * y).
An exact proof term for the current goal is sqrt_SNo_nonneg_prop1a x Hx Hxnonneg IH.
We prove the intermediate claim L1L: ∀w ∈ L, ∀p : prop, (SNo w → 0 ≤ w → w * w < x → p) → p.
Let w be given.
Assume Hw.
Let p be given.
Assume Hp.
Apply famunionE_impred ω L_ w Hw to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H1: w ∈ L_ k.
Apply L1 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.
An exact proof term for the current goal is Hp.
We prove the intermediate claim L1R: ∀z ∈ R, ∀p : prop, (SNo z → 0 ≤ z → x < z * z → p) → p.
Let z be given.
Assume Hz.
Let p be given.
Assume Hp.
Apply famunionE_impred ω R_ z Hz to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H1: z ∈ R_ k.
Apply L1 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.
An exact proof term for the current goal is Hp.
We prove the intermediate claim L2: SNoCutP L R.
An exact proof term for the current goal is sqrt_SNo_nonneg_prop1b x Hx Hxnonneg L1.
Apply L2 to the current goal.
Assume HLHR.
Apply HLHR to the current goal.
Assume HL: ∀w ∈ L, SNo w.
Assume HR: ∀z ∈ R, SNo z.
Assume HLR: ∀w ∈ L, ∀z ∈ R, w < z.
Set y to be the term SNoCut L R.
Apply SNoCutP_SNoCut_impred L R L2 to the current goal.
Assume H1: SNo y.
Assume H2: SNoLev y ∈ ordsucc ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Assume H3: ∀w ∈ L, w < y.
Assume H4: ∀z ∈ R, y < z.
Assume H5: ∀u, SNo u → (∀w ∈ L, w < u) → (∀z ∈ R, u < z) → SNoLev y ⊆ SNoLev u ∧ SNoEq_ (SNoLev y) y u.
We prove the intermediate claim Lynn: 0 ≤ y.
An exact proof term for the current goal is sqrt_SNo_nonneg_prop1c x Hx Hxnonneg L2 L1R.
We will prove SNo y ∧ 0 ≤ y ∧ y * y = x.
Apply and3I to the current goal.
We will prove SNo y.
An exact proof term for the current goal is H1.
We will prove 0 ≤ y.
An exact proof term for the current goal is Lynn.
We will prove y * y = x.
We prove the intermediate claim Lyy: SNo (y * y).
An exact proof term for the current goal is SNo_mul_SNo y y H1 H1.
We prove the intermediate claim Lyynn: 0 ≤ y * y.
An exact proof term for the current goal is mul_SNo_nonneg_nonneg y y H1 H1 Lynn Lynn.
Apply SNoLt_trichotomy_or_impred (y * y) x Lyy Hx to the current goal.
Assume H6: y * y < x.
We will prove False.
An exact proof term for the current goal is sqrt_SNo_nonneg_prop1d x Hx Hxnonneg IH L2 Lynn H6.
Assume H6: y * y = x.
An exact proof term for the current goal is H6.
Assume H6: x < y * y.
We will prove False.
An exact proof term for the current goal is sqrt_SNo_nonneg_prop1e x Hx Hxnonneg IH L2 Lynn H6.
∎