Let x be given.
Assume Hx Hxnn.
Apply real_E x Hx to the current goal.
Assume Hx1: SNo x.
Assume Hx2: SNoLev x ∈ ordsucc ω.
Assume Hx3: x ∈ SNoS_ (ordsucc ω).
Assume Hx4: - ω < x.
Assume Hx5: x < ω.
Assume Hx6: ∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x.
Assume Hx7: ∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k.
Apply sqrt_SNo_nonneg_prop1 x Hx1 Hxnn to the current goal.
Assume H.
Apply H to the current goal.
Assume H1: SNo (sqrt_SNo_nonneg x).
Assume H2: 0 ≤ sqrt_SNo_nonneg x.
Assume H3: sqrt_SNo_nonneg x * sqrt_SNo_nonneg x = x.
Apply ordsuccE ω (SNoLev x) Hx2 to the current goal.
Assume H4: SNoLev x ∈ ω.
We will prove sqrt_SNo_nonneg x ∈ real.
Apply sqrt_SNo_nonneg_SNoS_omega to the current goal.
We will prove x ∈ SNoS_ ω.
Apply SNoS_I ω omega_ordinal x (SNoLev x) H4 to the current goal.
We will prove SNo_ (SNoLev x) x.
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is Hx1.
We will prove 0 ≤ x.
An exact proof term for the current goal is Hxnn.
Assume H4: SNoLev x = ω.
We will prove sqrt_SNo_nonneg x ∈ real.
rewrite the current goal using sqrt_SNo_nonneg_eq x Hx1 (from left to right).
Set L_ to be the term λk : set ⇒ SNo_sqrtaux x sqrt_SNo_nonneg k 0.
Set R_ to be the term λk : set ⇒ SNo_sqrtaux x sqrt_SNo_nonneg k 1.
Set L to be the term ⋃k ∈ ωL_ k.
Set R to be the term ⋃k ∈ ωR_ k.
We will prove SNoCut L R ∈ real.
We prove the intermediate claim LLI: ∀k ∈ ω, SNo_sqrtaux x sqrt_SNo_nonneg k 0 ⊆ L.
Let k be given.
Assume Hk.
Let w be given.
Assume Hw.
We will prove w ∈ ⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 0.
An exact proof term for the current goal is famunionI ω (λk ⇒ SNo_sqrtaux x sqrt_SNo_nonneg k 0) k w Hk Hw.
We prove the intermediate claim LRI: ∀k ∈ ω, SNo_sqrtaux x sqrt_SNo_nonneg k 1 ⊆ R.
Let k be given.
Assume Hk.
Let z be given.
Assume Hz.
We will prove z ∈ ⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 1.
An exact proof term for the current goal is famunionI ω (λk ⇒ SNo_sqrtaux x sqrt_SNo_nonneg k 1) k z Hk Hz.
We prove the intermediate claim LLE: ∀w ∈ L, ∀p : prop, (∀k ∈ ω, w ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 0 → p) → p.
Let w be given.
Assume Hw: w ∈ L.
Let p be given.
Assume Hp.
Apply famunionE_impred ω (λk ⇒ SNo_sqrtaux x sqrt_SNo_nonneg k 0) w Hw to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume Hwk: w ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 0.
An exact proof term for the current goal is Hp k Hk Hwk.
We prove the intermediate claim LRE: ∀z ∈ R, ∀p : prop, (∀k ∈ ω, z ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 1 → p) → p.
Let z be given.
Assume Hz: z ∈ R.
Let p be given.
Assume Hp.
Apply famunionE_impred ω (λk ⇒ SNo_sqrtaux x sqrt_SNo_nonneg k 1) z Hz to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume Hzk: z ∈ SNo_sqrtaux x sqrt_SNo_nonneg k 1.
An exact proof term for the current goal is Hp k Hk Hzk.
We prove the intermediate claim L_L_Subq: ∀k, nat_p k → L_ k ⊆ L_ (ordsucc k).
Let k be given.
Assume Hk.
Let w be given.
Assume Hw: w ∈ L_ k.
We will prove w ∈ SNo_sqrtaux x sqrt_SNo_nonneg (ordsucc k) 0.
rewrite the current goal using SNo_sqrtaux_S x sqrt_SNo_nonneg k Hk (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
Apply binunionI1 to the current goal.
An exact proof term for the current goal is Hw.
We prove the intermediate claim L_R_Subq: ∀k, nat_p k → R_ k ⊆ R_ (ordsucc k).
Let k be given.
Assume Hk.
Let w be given.
Assume Hw: w ∈ R_ k.
We will prove w ∈ SNo_sqrtaux x sqrt_SNo_nonneg (ordsucc k) 1.
rewrite the current goal using SNo_sqrtaux_S x sqrt_SNo_nonneg k Hk (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
Apply binunionI1 to the current goal.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is Hw.
We prove the intermediate claim L_L_R_Subq: ∀k, nat_p k → ∀k' ∈ k, L_ k' ⊆ L_ k ∧ R_ k' ⊆ R_ k.
We will prove ∀k, nat_p k → ∀k' ∈ k, SNo_sqrtaux x sqrt_SNo_nonneg k' 0 ⊆ SNo_sqrtaux x sqrt_SNo_nonneg k 0 ∧ SNo_sqrtaux x sqrt_SNo_nonneg k' 1 ⊆ SNo_sqrtaux x sqrt_SNo_nonneg k 1.
Apply nat_ind to the current goal.
Let k' be given.
Assume Hk': k' ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE k' Hk'.
Let k be given.
Assume Hk.
Assume IHk: ∀k' ∈ k, L_ k' ⊆ L_ k ∧ R_ k' ⊆ R_ k.
Let k' be given.
Assume Hk': k' ∈ ordsucc k.
Apply ordsuccE k k' Hk' to the current goal.
Assume Hk'2: k' ∈ k.
Apply IHk k' Hk'2 to the current goal.
Assume IHkL IHkR.
Apply andI to the current goal.
We will prove L_ k' ⊆ L_ (ordsucc k).
Apply Subq_tra (L_ k') (L_ k) (L_ (ordsucc k)) IHkL to the current goal.
We will prove L_ k ⊆ L_ (ordsucc k).
An exact proof term for the current goal is L_L_Subq k Hk.
We will prove R_ k' ⊆ R_ (ordsucc k).
Apply Subq_tra (R_ k') (R_ k) (R_ (ordsucc k)) IHkR to the current goal.
We will prove R_ k ⊆ R_ (ordsucc k).
An exact proof term for the current goal is L_R_Subq k Hk.
Assume Hk'2: k' = k.
rewrite the current goal using Hk'2 (from left to right).
Apply andI to the current goal.
We will prove L_ k ⊆ L_ (ordsucc k).
An exact proof term for the current goal is L_L_Subq k Hk.
We will prove R_ k ⊆ R_ (ordsucc k).
An exact proof term for the current goal is L_R_Subq k Hk.
We prove the intermediate claim L_L_R_real: ∀k, nat_p k → L_ k ⊆ {w ∈ real|0 ≤ w} ∧ R_ k ⊆ {w ∈ real|0 ≤ w}.
We will prove ∀k, nat_p k → SNo_sqrtaux x sqrt_SNo_nonneg k 0 ⊆ {w ∈ real|0 ≤ w} ∧ SNo_sqrtaux x sqrt_SNo_nonneg k 1 ⊆ {w ∈ real|0 ≤ w}.
Apply nat_ind to the current goal.
rewrite the current goal using SNo_sqrtaux_0 (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
Apply andI to the current goal.
We will prove {sqrt_SNo_nonneg w|w ∈ SNoL_nonneg x} ⊆ {w ∈ real|0 ≤ w}.
Let w' be given.
Assume Hw'.
Apply ReplE_impred (SNoL_nonneg x) sqrt_SNo_nonneg w' Hw' to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL_nonneg x.
Assume Hw'w: w' = sqrt_SNo_nonneg w.
rewrite the current goal using Hw'w (from left to right).
We will prove sqrt_SNo_nonneg w ∈ {w ∈ real|0 ≤ w}.
Apply SepE (SNoL x) (λw ⇒ 0 ≤ w) w Hw to the current goal.
Assume Hw1: w ∈ SNoL x.
Assume Hwnneg: 0 ≤ w.
Apply SNoL_E x Hx1 w Hw1 to the current goal.
Assume Hw1a Hw1b Hw1c.
Apply SepI to the current goal.
Apply sqrt_SNo_nonneg_SNoS_omega to the current goal.
We will prove w ∈ SNoS_ ω.
Apply SNoS_I ω omega_ordinal w (SNoLev w) to the current goal.
We will prove SNoLev w ∈ ω.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is Hw1b.
We will prove SNo_ (SNoLev w) w.
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is Hw1a.
We will prove 0 ≤ w.
An exact proof term for the current goal is Hwnneg.
We will prove 0 ≤ sqrt_SNo_nonneg w.
An exact proof term for the current goal is sqrt_SNo_nonneg_nonneg w Hw1a Hwnneg.
We will prove {sqrt_SNo_nonneg z|z ∈ SNoR x} ⊆ {w ∈ real|0 ≤ w}.
Let z' be given.
Assume Hz'.
Apply ReplE_impred (SNoR x) sqrt_SNo_nonneg z' Hz' to the current goal.
Let z be given.
Assume Hz: z ∈ SNoR x.
Assume Hz'z: z' = sqrt_SNo_nonneg z.
rewrite the current goal using Hz'z (from left to right).
We will prove sqrt_SNo_nonneg z ∈ {z ∈ real|0 ≤ z}.
Apply SNoR_E x Hx1 z Hz to the current goal.
Assume Hz1 Hz2 Hz3.
Apply SepI to the current goal.
Apply sqrt_SNo_nonneg_SNoS_omega to the current goal.
We will prove z ∈ SNoS_ ω.
Apply SNoS_I ω omega_ordinal z (SNoLev z) to the current goal.
We will prove SNoLev z ∈ ω.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is Hz2.
We will prove SNo_ (SNoLev z) z.
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is Hz1.
We will prove 0 ≤ z.
Apply SNoLtLe to the current goal.
We will prove 0 < z.
An exact proof term for the current goal is SNoLeLt_tra 0 x z SNo_0 Hx1 Hz1 Hxnn Hz3.
We will prove 0 ≤ sqrt_SNo_nonneg z.
Apply sqrt_SNo_nonneg_nonneg z Hz1 to the current goal.
We will prove 0 ≤ z.
Apply SNoLtLe to the current goal.
We will prove 0 < z.
An exact proof term for the current goal is SNoLeLt_tra 0 x z SNo_0 Hx1 Hz1 Hxnn Hz3.
Let k be given.
Assume Hk.
Assume IHk.
Apply IHk to the current goal.
Assume IHk0: SNo_sqrtaux x sqrt_SNo_nonneg k 0 ⊆ {w ∈ real|0 ≤ w}.
Assume IHk1: SNo_sqrtaux x sqrt_SNo_nonneg k 1 ⊆ {w ∈ real|0 ≤ w}.
rewrite the current goal using SNo_sqrtaux_S x sqrt_SNo_nonneg k Hk (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
Apply andI to the current goal.
We will prove SNo_sqrtaux x sqrt_SNo_nonneg k 0 ∪ SNo_sqrtauxset (SNo_sqrtaux x sqrt_SNo_nonneg k 0) (SNo_sqrtaux x sqrt_SNo_nonneg k 1) x ⊆ {w ∈ real|0 ≤ w}.
Apply binunion_Subq_min to the current goal.
An exact proof term for the current goal is IHk0.
We will prove SNo_sqrtauxset (SNo_sqrtaux x sqrt_SNo_nonneg k 0) (SNo_sqrtaux x sqrt_SNo_nonneg k 1) x ⊆ {w ∈ real|0 ≤ w}.
Apply SNo_sqrtauxset_real_nonneg to the current goal.
An exact proof term for the current goal is IHk0.
An exact proof term for the current goal is IHk1.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hxnn.
We will prove SNo_sqrtaux x sqrt_SNo_nonneg k 1 ∪ SNo_sqrtauxset (SNo_sqrtaux x sqrt_SNo_nonneg k 0) (SNo_sqrtaux x sqrt_SNo_nonneg k 0) x ∪ SNo_sqrtauxset (SNo_sqrtaux x sqrt_SNo_nonneg k 1) (SNo_sqrtaux x sqrt_SNo_nonneg k 1) x ⊆ {w ∈ real|0 ≤ w}.
Apply binunion_Subq_min to the current goal.
Apply binunion_Subq_min to the current goal.
An exact proof term for the current goal is IHk1.
We will prove SNo_sqrtauxset (SNo_sqrtaux x sqrt_SNo_nonneg k 0) (SNo_sqrtaux x sqrt_SNo_nonneg k 0) x ⊆ {w ∈ real|0 ≤ w}.
Apply SNo_sqrtauxset_real_nonneg to the current goal.
An exact proof term for the current goal is IHk0.
An exact proof term for the current goal is IHk0.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hxnn.
We will prove SNo_sqrtauxset (SNo_sqrtaux x sqrt_SNo_nonneg k 1) (SNo_sqrtaux x sqrt_SNo_nonneg k 1) x ⊆ {w ∈ real|0 ≤ w}.
Apply SNo_sqrtauxset_real_nonneg to the current goal.
An exact proof term for the current goal is IHk1.
An exact proof term for the current goal is IHk1.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hxnn.
We prove the intermediate claim LLsR: L ⊆ real.
Let w be given.
Assume Hw.
Apply LLE w Hw to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume Hwk: w ∈ L_ k.
Apply L_L_R_real k (omega_nat_p k Hk) to the current goal.
Assume H _.
An exact proof term for the current goal is SepE1 real (λw ⇒ 0 ≤ w) w (H w Hwk).
We prove the intermediate claim LRsR: R ⊆ real.
Let z be given.
Assume Hz.
Apply LRE z Hz to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume Hzk: z ∈ R_ k.
Apply L_L_R_real k (omega_nat_p k Hk) to the current goal.
Assume _ H.
An exact proof term for the current goal is SepE1 real (λw ⇒ 0 ≤ w) z (H z Hzk).
We prove the intermediate claim LLR: SNoCutP L R.
An exact proof term for the current goal is SNo_sqrt_SNo_SNoCutP x Hx1 Hxnn.
Apply SNoCutP_SNoCut_impred L R LLR to the current goal.
rewrite the current goal using sqrt_SNo_nonneg_eq x Hx1 (from right to left).
Assume HLR1 HLR2.
Assume HLR3: ∀w ∈ L, w < sqrt_SNo_nonneg x.
Assume HLR4: ∀z ∈ R, sqrt_SNo_nonneg x < z.
Assume HLR5.
We prove the intermediate claim L0Lx: 0 ∈ SNoLev x.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is nat_p_omega 0 nat_0.
We prove the intermediate claim L1Lx: 1 ∈ SNoLev x.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is nat_p_omega 1 nat_1.
We prove the intermediate claim LLne: L ≠ 0.
An exact proof term for the current goal is sqrt_SNo_nonneg_Lnonempty x Hx1 Hxnn L0Lx.
We prove the intermediate claim LRne: R ≠ 0.
An exact proof term for the current goal is sqrt_SNo_nonneg_Rnonempty x Hx1 Hxnn L1Lx.
We will prove SNoCut L R ∈ real.
We prove the intermediate claim LRE': ∀z ∈ R, SNo z ∧ 0 < z.
Let z be given.
Assume Hz.
We prove the intermediate claim LzS: SNo z.
An exact proof term for the current goal is real_SNo z (LRsR z Hz).
Apply andI to the current goal.
An exact proof term for the current goal is LzS.
Apply SNoLeLt_tra 0 (sqrt_SNo_nonneg x) z SNo_0 H1 LzS to the current goal.
We will prove 0 ≤ sqrt_SNo_nonneg x.
An exact proof term for the current goal is H2.
We will prove sqrt_SNo_nonneg x < z.
An exact proof term for the current goal is HLR4 z Hz.
We prove the intermediate claim LLnomax: ∀w ∈ L, ∃w' ∈ L, w < w'.
Let w be given.
Assume Hw.
Apply LLE w Hw to the current goal.
Let k be given.
Assume Hk.
Assume Hwk: w ∈ L_ k.
Apply L_L_R_real k (omega_nat_p k Hk) to the current goal.
Assume H _.
Apply SepE real (λw ⇒ 0 ≤ w) w (H w Hwk) to the current goal.
Assume HwR: w ∈ real.
Assume Hwnn: 0 ≤ w.
We prove the intermediate claim Lw: SNo w.
An exact proof term for the current goal is real_SNo w HwR.
Apply xm (∃z, z ∈ R) to the current goal.
Assume H5.
Apply H5 to the current goal.
Let z be given.
Assume Hz: z ∈ R.
Apply LRE z Hz to the current goal.
Let k' be given.
Assume Hk'.
Assume Hzk': z ∈ R_ k'.
Apply LRE' z Hz to the current goal.
Assume HzS: SNo z.
Assume Hzpos: 0 < z.
Apply L_L_R_real k' (omega_nat_p k' Hk') to the current goal.
Assume _ H.
We prove the intermediate claim LzR: z ∈ real.
An exact proof term for the current goal is SepE1 real (λw ⇒ 0 ≤ w) z (H z Hzk').
We prove the intermediate claim Lz: SNo z.
An exact proof term for the current goal is real_SNo z LzR.
We prove the intermediate claim Lzpos: 0 < z.
Apply SNoLeLt_tra 0 (sqrt_SNo_nonneg x) z SNo_0 H1 Lz to the current goal.
We will prove 0 ≤ sqrt_SNo_nonneg x.
An exact proof term for the current goal is H2.
We will prove sqrt_SNo_nonneg x < z.
An exact proof term for the current goal is HLR4 z Hz.
We prove the intermediate claim Lwz: SNo (w + z).
An exact proof term for the current goal is SNo_add_SNo w z Lw Lz.
We prove the intermediate claim Lwmz: SNo (w * z).
An exact proof term for the current goal is SNo_mul_SNo w z Lw Lz.
We prove the intermediate claim Lwzpos: 0 < w + z.
rewrite the current goal using add_SNo_0R 0 SNo_0 (from right to left).
Apply add_SNo_Lt3b 0 0 w z SNo_0 SNo_0 Lw Lz Hwnn to the current goal.
We will prove 0 < z.
An exact proof term for the current goal is Lzpos.
Set w' to be the term (x + w * z) :/: (w + z).
We use w' to witness the existential quantifier.
Apply andI to the current goal.
We will prove w' ∈ L.
We prove the intermediate claim Lwzk'': ∃k'' ∈ ω, w ∈ L_ k'' ∧ z ∈ R_ k''.
Apply ordinal_trichotomy_or_impred k k' (nat_p_ordinal k (omega_nat_p k Hk)) (nat_p_ordinal k' (omega_nat_p k' Hk')) to the current goal.
Assume H6: k ∈ k'.
We use k' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk'.
Apply andI to the current goal.
We will prove w ∈ L_ k'.
Apply L_L_R_Subq k' (omega_nat_p k' Hk') k H6 to the current goal.
Assume H _.
An exact proof term for the current goal is H w Hwk.
An exact proof term for the current goal is Hzk'.
Assume H6: k = k'.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk.
Apply andI to the current goal.
An exact proof term for the current goal is Hwk.
We will prove z ∈ R_ k.
rewrite the current goal using H6 (from left to right).
An exact proof term for the current goal is Hzk'.
Assume H6: k' ∈ k.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk.
Apply andI to the current goal.
An exact proof term for the current goal is Hwk.
We will prove z ∈ R_ k.
Apply L_L_R_Subq k (omega_nat_p k Hk) k' H6 to the current goal.
Assume _ H.
An exact proof term for the current goal is H z Hzk'.
Apply Lwzk'' to the current goal.
Let k'' be given.
Assume H.
Apply H to the current goal.
Assume Hk'': k'' ∈ ω.
Assume H.
Apply H to the current goal.
Assume Hwk'': w ∈ L_ k''.
Assume Hzk'': z ∈ R_ k''.
We prove the intermediate claim Lw'LSk'': w' ∈ L_ (ordsucc k'').
We will prove w' ∈ SNo_sqrtaux x sqrt_SNo_nonneg (ordsucc k'') 0.
rewrite the current goal using SNo_sqrtaux_S x sqrt_SNo_nonneg k'' (omega_nat_p k'' Hk'') (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
Apply binunionI2 to the current goal.
We will prove w' ∈ SNo_sqrtauxset (L_ k'') (R_ k'') x.
Apply SNo_sqrtauxset_I to the current goal.
An exact proof term for the current goal is Hwk''.
An exact proof term for the current goal is Hzk''.
We will prove 0 < w + z.
An exact proof term for the current goal is Lwzpos.
An exact proof term for the current goal is famunionI ω L_ (ordsucc k'') w' (omega_ordsucc k'' Hk'') Lw'LSk''.
We will prove w < w'.
We will prove w < (x + w * z) :/: (w + z).
Apply div_SNo_pos_LtR (x + w * z) (w + z) w (SNo_add_SNo x (w * z) Hx1 Lwmz) Lwz Lw Lwzpos to the current goal.
We will prove w * (w + z) < x + w * z.
rewrite the current goal using mul_SNo_distrL w w z Lw Lw HzS (from left to right).
We will prove w * w + w * z < x + w * z.
Apply add_SNo_Lt1 (w * w) (w * z) x (SNo_mul_SNo w w Lw Lw) (SNo_mul_SNo w z Lw HzS) Hx1 to the current goal.
We will prove w * w < x.
rewrite the current goal using H3 (from right to left).
We will prove w * w < sqrt_SNo_nonneg x * sqrt_SNo_nonneg x.
We prove the intermediate claim Lwsx: w < sqrt_SNo_nonneg x.
An exact proof term for the current goal is HLR3 w Hw.
Apply SNoLeE 0 w SNo_0 Lw Hwnn to the current goal.
Assume H6: 0 < w.
An exact proof term for the current goal is pos_mul_SNo_Lt2 w w (sqrt_SNo_nonneg x) (sqrt_SNo_nonneg x) Lw Lw H1 H1 H6 H6 Lwsx Lwsx.
Assume H6: 0 = w.
rewrite the current goal using H6 (from right to left).
rewrite the current goal using mul_SNo_zeroR 0 SNo_0 (from left to right).
We will prove 0 < sqrt_SNo_nonneg x * sqrt_SNo_nonneg x.
We prove the intermediate claim Lsxpos: 0 < sqrt_SNo_nonneg x.
rewrite the current goal using H6 (from left to right).
An exact proof term for the current goal is Lwsx.
An exact proof term for the current goal is mul_SNo_pos_pos (sqrt_SNo_nonneg x) (sqrt_SNo_nonneg x) H1 H1 Lsxpos Lsxpos.
Assume H5: ¬ ∃z, z ∈ R.
Apply LRne to the current goal.
Apply Empty_eq to the current goal.
Let z be given.
Assume Hz.
Apply H5 to the current goal.
We use z to witness the existential quantifier.
An exact proof term for the current goal is Hz.
We prove the intermediate claim LRnomin: ∀z ∈ R, ∃z' ∈ R, z' < z.
Let z be given.
Assume Hz.
Apply LRE z Hz to the current goal.
Let k be given.
Assume Hk.
Assume Hzk: z ∈ R_ k.
Apply LRE' z Hz to the current goal.
Assume HzS: SNo z.
Assume Hzpos: 0 < z.
We prove the intermediate claim Lzz: SNo (z + z).
An exact proof term for the current goal is SNo_add_SNo z z HzS HzS.
We prove the intermediate claim Lzzpos: 0 < z + z.
rewrite the current goal using add_SNo_0R 0 SNo_0 (from right to left).
We will prove 0 + 0 < z + z.
An exact proof term for the current goal is add_SNo_Lt3 0 0 z z SNo_0 SNo_0 HzS HzS Hzpos Hzpos.
We prove the intermediate claim Lzzn0: z + z ≠ 0.
Assume H5.
Apply SNoLt_irref 0 to the current goal.
rewrite the current goal using H5 (from right to left) at position 2.
An exact proof term for the current goal is Lzzpos.
We prove the intermediate claim Lzmz: SNo (z * z).
An exact proof term for the current goal is SNo_mul_SNo z z HzS HzS.
Set z' to be the term (x + z * z) :/: (z + z).
We prove the intermediate claim Lz': z' ∈ R_ (ordsucc k).
We will prove z' ∈ SNo_sqrtaux x sqrt_SNo_nonneg (ordsucc k) 1.
rewrite the current goal using SNo_sqrtaux_S x sqrt_SNo_nonneg k (omega_nat_p k Hk) (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
Apply binunionI2 to the current goal.
We will prove (x + z * z) :/: (z + z) ∈ SNo_sqrtauxset (SNo_sqrtaux x sqrt_SNo_nonneg k 1) (SNo_sqrtaux x sqrt_SNo_nonneg k 1) x.
Apply SNo_sqrtauxset_I to the current goal.
We will prove z ∈ R_ k.
An exact proof term for the current goal is Hzk.
We will prove z ∈ R_ k.
An exact proof term for the current goal is Hzk.
We will prove 0 < z + z.
An exact proof term for the current goal is Lzzpos.
We prove the intermediate claim Lz'R: z' ∈ R.
An exact proof term for the current goal is famunionI ω R_ (ordsucc k) z' (omega_ordsucc k Hk) Lz'.
We prove the intermediate claim Lz'S: SNo z'.
An exact proof term for the current goal is real_SNo z' (LRsR z' Lz'R).
We use z' to witness the existential quantifier.
Apply andI to the current goal.
We will prove z' ∈ R.
An exact proof term for the current goal is Lz'R.
We will prove z' < z.
We will prove (x + z * z) :/: (z + z) < z.
Apply div_SNo_pos_LtL (x + z * z) (z + z) z (SNo_add_SNo x (z * z) Hx1 Lzmz) Lzz HzS Lzzpos to the current goal.
We will prove x + z * z < z * (z + z).
rewrite the current goal using mul_SNo_distrL z z z HzS HzS HzS (from left to right).
We will prove x + z * z < z * z + z * z.
Apply add_SNo_Lt1 x (z * z) (z * z) Hx1 Lzmz Lzmz to the current goal.
We will prove x < z * z.
rewrite the current goal using H3 (from right to left).
We will prove sqrt_SNo_nonneg x * sqrt_SNo_nonneg x < z * z.
Apply SNoLeE 0 (sqrt_SNo_nonneg x) SNo_0 H1 H2 to the current goal.
Assume Hsxpos: 0 < sqrt_SNo_nonneg x.
An exact proof term for the current goal is pos_mul_SNo_Lt2 (sqrt_SNo_nonneg x) (sqrt_SNo_nonneg x) z z H1 H1 HzS HzS Hsxpos Hsxpos (HLR4 z Hz) (HLR4 z Hz).
Assume Hsx0: 0 = sqrt_SNo_nonneg x.
rewrite the current goal using Hsx0 (from right to left).
rewrite the current goal using mul_SNo_zeroR 0 SNo_0 (from left to right).
We will prove 0 < z * z.
An exact proof term for the current goal is mul_SNo_pos_pos z z HzS HzS Hzpos Hzpos.
An exact proof term for the current goal is real_SNoCut L LLsR R LRsR LLR LLne LRne LLnomax LRnomin.
∎