Apply SNoLev_ind to the current goal.
Let x be given.
Assume Hx: SNo x.
Assume IHx: ∀u ∈ SNoS_ (SNoLev x), u ∈ real → 0 < u → recip_SNo_pos u ∈ real ∧ ∀k, nat_p k → (∀y ∈ SNo_recipaux u recip_SNo_pos k 0, y ∈ real) ∧ (∀y ∈ SNo_recipaux u recip_SNo_pos k 1, y ∈ real).
Assume HxR: x ∈ real.
Assume Hxpos: 0 < x.
Apply real_E x HxR to the current goal.
Assume _.
Assume HxR2: SNoLev x ∈ ordsucc ω.
Assume _ _ _ _ _.
We prove the intermediate claim Lmx: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Hx.
We prove the intermediate claim L1: ∀y ∈ real, ∀z ∈ SNoS_ (SNoLev x), 0 < z → (1 + (z + - x) * y) * recip_SNo_pos z ∈ real.
Let y be given.
Assume Hy.
Let z be given.
Assume Hz Hzpos.
Apply SNoS_E2 (SNoLev x) (SNoLev_ordinal x Hx) z Hz to the current goal.
Assume Hz1: SNoLev z ∈ SNoLev x.
Assume Hz2: ordinal (SNoLev z).
Assume Hz3: SNo z.
Assume Hz4: SNo_ (SNoLev z) z.
We prove the intermediate claim LzR: z ∈ real.
Apply SNoS_omega_real to the current goal.
Apply SNoS_I ω omega_ordinal z (SNoLev z) to the current goal.
We will prove SNoLev z ∈ ω.
Apply ordsuccE ω (SNoLev x) HxR2 to the current goal.
Assume H1: SNoLev x ∈ ω.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_p_trans (SNoLev x) (omega_nat_p (SNoLev x) H1) (SNoLev z) Hz1.
Assume H1: SNoLev x = ω.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hz1.
An exact proof term for the current goal is Hz4.
Apply IHx z Hz LzR Hzpos to the current goal.
Assume IH1: recip_SNo_pos z ∈ real.
Assume _.
Apply real_mul_SNo to the current goal.
Apply real_add_SNo to the current goal.
An exact proof term for the current goal is real_1.
Apply real_mul_SNo to the current goal.
Apply real_add_SNo to the current goal.
An exact proof term for the current goal is LzR.
Apply real_minus_SNo to the current goal.
An exact proof term for the current goal is HxR.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is IH1.
We prove the intermediate claim L2: ∀k, nat_p k → (SNo_recipaux x recip_SNo_pos k 0 ⊆ real) ∧ (SNo_recipaux x recip_SNo_pos k 1 ⊆ real).
Apply nat_ind to the current goal.
We will prove (SNo_recipaux x recip_SNo_pos 0 0 ⊆ real) ∧ (SNo_recipaux x recip_SNo_pos 0 1 ⊆ real).
rewrite the current goal using SNo_recipaux_0 (from left to right).
Apply andI to the current goal.
rewrite the current goal using tuple_2_0_eq (from left to right).
Let y be given.
Assume Hy: y ∈ {0}.
rewrite the current goal using SingE 0 y Hy (from left to right).
We will prove 0 ∈ real.
An exact proof term for the current goal is real_0.
rewrite the current goal using tuple_2_1_eq (from left to right).
Let y be given.
Assume Hy: y ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE y Hy.
Let k be given.
Assume Hk: nat_p k.
Assume IHk: (SNo_recipaux x recip_SNo_pos k 0 ⊆ real) ∧ (SNo_recipaux x recip_SNo_pos k 1 ⊆ real).
Apply IHk to the current goal.
Assume IHk0 IHk1.
rewrite the current goal using SNo_recipaux_S x recip_SNo_pos k Hk (from left to right).
Apply andI to the current goal.
rewrite the current goal using tuple_2_0_eq (from left to right).
Let y be given.
Apply binunionE' to the current goal.
Apply binunionE' to the current goal.
An exact proof term for the current goal is IHk0 y.
Assume Hy: y ∈ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 0) x (SNoR x) recip_SNo_pos.
Apply SNo_recipauxset_E (SNo_recipaux x recip_SNo_pos k 0) x (SNoR x) recip_SNo_pos y Hy to the current goal.
Let u be given.
Assume Hu: u ∈ SNo_recipaux x recip_SNo_pos k 0.
Let z be given.
Assume Hz: z ∈ SNoR x.
Assume Hye: y = (1 + (z + - x) * u) * recip_SNo_pos z.
Apply SNoR_E x Hx z Hz to the current goal.
Assume Hz1: SNo z.
Assume Hz2: SNoLev z ∈ SNoLev x.
Assume Hz3: x < z.
rewrite the current goal using Hye (from left to right).
Apply L1 to the current goal.
We will prove u ∈ real.
An exact proof term for the current goal is IHk0 u Hu.
We will prove z ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 z x Hz1 Hx Hz2.
We will prove 0 < z.
An exact proof term for the current goal is SNoLt_tra 0 x z SNo_0 Hx Hz1 Hxpos Hz3.
Assume Hy: y ∈ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 1) x (SNoL_pos x) recip_SNo_pos.
Apply SNo_recipauxset_E (SNo_recipaux x recip_SNo_pos k 1) x (SNoL_pos x) recip_SNo_pos y Hy to the current goal.
Let u be given.
Assume Hu: u ∈ SNo_recipaux x recip_SNo_pos k 1.
Let w be given.
Assume Hw: w ∈ SNoL_pos x.
Assume Hye: y = (1 + (w + - x) * u) * recip_SNo_pos w.
Apply SepE (SNoL x) (λw ⇒ 0 < w) w Hw to the current goal.
Assume Hw0: w ∈ SNoL x.
Assume Hwpos: 0 < w.
Apply SNoL_E x Hx w Hw0 to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev x.
Assume Hw3: w < x.
rewrite the current goal using Hye (from left to right).
Apply L1 to the current goal.
We will prove u ∈ real.
An exact proof term for the current goal is IHk1 u Hu.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
We will prove 0 < w.
An exact proof term for the current goal is Hwpos.
rewrite the current goal using tuple_2_1_eq (from left to right).
Let y be given.
Apply binunionE' to the current goal.
Apply binunionE' to the current goal.
An exact proof term for the current goal is IHk1 y.
Assume Hy: y ∈ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 0) x (SNoL_pos x) recip_SNo_pos.
Apply SNo_recipauxset_E (SNo_recipaux x recip_SNo_pos k 0) x (SNoL_pos x) recip_SNo_pos y Hy to the current goal.
Let u be given.
Assume Hu: u ∈ SNo_recipaux x recip_SNo_pos k 0.
Let w be given.
Assume Hw: w ∈ SNoL_pos x.
Assume Hye: y = (1 + (w + - x) * u) * recip_SNo_pos w.
Apply SepE (SNoL x) (λw ⇒ 0 < w) w Hw to the current goal.
Assume Hw0: w ∈ SNoL x.
Assume Hwpos: 0 < w.
Apply SNoL_E x Hx w Hw0 to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev x.
Assume Hw3: w < x.
rewrite the current goal using Hye (from left to right).
Apply L1 to the current goal.
We will prove u ∈ real.
An exact proof term for the current goal is IHk0 u Hu.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
We will prove 0 < w.
An exact proof term for the current goal is Hwpos.
Assume Hy: y ∈ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 1) x (SNoR x) recip_SNo_pos.
Apply SNo_recipauxset_E (SNo_recipaux x recip_SNo_pos k 1) x (SNoR x) recip_SNo_pos y Hy to the current goal.
Let u be given.
Assume Hu: u ∈ SNo_recipaux x recip_SNo_pos k 1.
Let z be given.
Assume Hz: z ∈ SNoR x.
Assume Hye: y = (1 + (z + - x) * u) * recip_SNo_pos z.
Apply SNoR_E x Hx z Hz to the current goal.
Assume Hz1: SNo z.
Assume Hz2: SNoLev z ∈ SNoLev x.
Assume Hz3: x < z.
rewrite the current goal using Hye (from left to right).
Apply L1 to the current goal.
We will prove u ∈ real.
An exact proof term for the current goal is IHk1 u Hu.
We will prove z ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 z x Hz1 Hx Hz2.
We will prove 0 < z.
An exact proof term for the current goal is SNoLt_tra 0 x z SNo_0 Hx Hz1 Hxpos Hz3.
Apply andI to the current goal.
We will prove recip_SNo_pos x ∈ real.
We prove the intermediate claim L3: ∀u ∈ SNoS_ (SNoLev x), 0 < u → SNo (recip_SNo_pos u) ∧ u * recip_SNo_pos u = 1.
Let u be given.
Assume Hu Hupos.
Apply SNoS_E2 (SNoLev x) (SNoLev_ordinal x Hx) u Hu to the current goal.
Assume _ _.
Assume Hu1: SNo u.
Assume _.
An exact proof term for the current goal is recip_SNo_pos_prop1 u Hu1 Hupos.
Set L to be the term (⋃k ∈ ωSNo_recipaux x recip_SNo_pos k 0).
Set R to be the term (⋃k ∈ ωSNo_recipaux x recip_SNo_pos k 1).
We prove the intermediate claim LrxLR: recip_SNo_pos x = SNoCut L R.
An exact proof term for the current goal is recip_SNo_pos_eq x Hx.
We prove the intermediate claim LLR: SNoCutP L R.
An exact proof term for the current goal is SNo_recipaux_lem2 x Hx Hxpos recip_SNo_pos L3.
Apply SNoCutP_SNoCut_impred L R LLR to the current goal.
Set y to be the term SNoCut L R.
Assume HLR1: SNo y.
Assume HLR2: SNoLev y ∈ ordsucc ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Assume HLR3: ∀w ∈ L, w < y.
Assume HLR4: ∀z ∈ R, y < z.
Assume HLR5: ∀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 LLI: ∀k ∈ ω, SNo_recipaux x recip_SNo_pos k 0 ⊆ L.
Let k be given.
Assume Hk.
Let w be given.
Assume Hw.
We will prove w ∈ ⋃k ∈ ωSNo_recipaux x recip_SNo_pos k 0.
An exact proof term for the current goal is famunionI ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 0) k w Hk Hw.
We prove the intermediate claim LRI: ∀k ∈ ω, SNo_recipaux x recip_SNo_pos k 1 ⊆ R.
Let k be given.
Assume Hk.
Let z be given.
Assume Hz.
We will prove z ∈ ⋃k ∈ ωSNo_recipaux x recip_SNo_pos k 1.
An exact proof term for the current goal is famunionI ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 1) k z Hk Hz.
We prove the intermediate claim LLE: ∀w ∈ L, ∀p : prop, (∀k ∈ ω, w ∈ SNo_recipaux x recip_SNo_pos k 0 → p) → p.
Let w be given.
Assume Hw: w ∈ L.
Let p be given.
Assume Hp.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 0) w Hw to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume Hwk: w ∈ SNo_recipaux x recip_SNo_pos 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_recipaux x recip_SNo_pos k 1 → p) → p.
Let z be given.
Assume Hz: z ∈ R.
Let p be given.
Assume Hp.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 1) z Hz to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume Hzk: z ∈ SNo_recipaux x recip_SNo_pos k 1.
An exact proof term for the current goal is Hp k Hk Hzk.
We prove the intermediate claim LLreal: L ⊆ real.
Let w be given.
Assume Hw: w ∈ L.
Apply LLE w Hw to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume Hwk: w ∈ SNo_recipaux x recip_SNo_pos k 0.
Apply L2 k (omega_nat_p k Hk) to the current goal.
Assume H2: SNo_recipaux x recip_SNo_pos k 0 ⊆ real.
Assume _.
An exact proof term for the current goal is H2 w Hwk.
We prove the intermediate claim LRreal: R ⊆ real.
Let z be given.
Assume Hz: z ∈ R.
Apply LRE z Hz to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume Hzk: z ∈ SNo_recipaux x recip_SNo_pos k 1.
Apply L2 k (omega_nat_p k Hk) to the current goal.
Assume _.
Assume H2: SNo_recipaux x recip_SNo_pos k 1 ⊆ real.
An exact proof term for the current goal is H2 z Hzk.
We prove the intermediate claim LL0: L ≠ 0.
Assume H1: L = 0.
Apply EmptyE 0 to the current goal.
We will prove 0 ∈ 0.
rewrite the current goal using H1 (from right to left) at position 2.
We will prove 0 ∈ L.
Apply LLI 0 (nat_p_omega 0 nat_0) to the current goal.
We will prove 0 ∈ SNo_recipaux x recip_SNo_pos 0 0.
rewrite the current goal using SNo_recipaux_0 (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
We will prove 0 ∈ {0}.
Apply SingI to the current goal.
Apply xm (∃m ∈ ω, x = eps_ m) to the current goal.
Assume H.
Apply H to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ ω.
Assume H1: x = eps_ m.
We will prove recip_SNo_pos x ∈ real.
rewrite the current goal using H1 (from left to right).
We will prove recip_SNo_pos (eps_ m) ∈ real.
rewrite the current goal using recip_SNo_pos_eps_ m (omega_nat_p m Hm) (from left to right).
We will prove 2 ^ m ∈ real.
Apply SNoS_omega_real to the current goal.
Apply omega_SNoS_omega to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_exp_SNo_nat 2 nat_2 m (omega_nat_p m Hm).
Assume H1: ¬ (∃m ∈ ω, x = eps_ m).
Apply xm (x = 2) to the current goal.
Assume H2: x = 2.
rewrite the current goal using H2 (from left to right).
We will prove recip_SNo_pos 2 ∈ real.
rewrite the current goal using recip_SNo_pos_2 (from left to right).
We will prove eps_ 1 ∈ real.
Apply SNoS_omega_real to the current goal.
Apply SNo_eps_SNoS_omega to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_1.
Assume H2: x ≠ 2.
We prove the intermediate claim L4: ∀m ∈ ω, x ≠ eps_ m.
Let m be given.
Assume Hm H3.
Apply H1 to the current goal.
We use m to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hm.
An exact proof term for the current goal is H3.
Apply pos_real_left_approx_double x HxR Hxpos H2 L4 to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Assume Hu: u ∈ SNoL_pos x.
Apply SepE (SNoL x) (λw ⇒ 0 < w) u Hu to the current goal.
Assume Hua: u ∈ SNoL x.
Assume Hub: 0 < u.
Apply SNoL_E x Hx u Hua to the current goal.
Assume Hua1: SNo u.
Assume Hua2: SNoLev u ∈ SNoLev x.
Assume Hua3: u < x.
Assume H3: x < 2 * u.
We prove the intermediate claim Lru: SNo (recip_SNo_pos u).
An exact proof term for the current goal is SNo_recip_SNo_pos u Hua1 Hub.
We prove the intermediate claim Lumx: SNo (u + - x).
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hua1.
An exact proof term for the current goal is Lmx.
Set f to be the term λv ⇒ (1 + (u + - x) * v) * recip_SNo_pos u of type set → set.
We prove the intermediate claim L5: ∀w ∈ L, f w ∈ R.
Let w be given.
Assume Hw.
Apply LLE w Hw to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume Hwk: w ∈ SNo_recipaux x recip_SNo_pos k 0.
Apply LRI (ordsucc k) (omega_ordsucc k Hk) to the current goal.
We will prove f w ∈ SNo_recipaux x recip_SNo_pos (ordsucc k) 1.
rewrite the current goal using SNo_recipaux_S x recip_SNo_pos k (omega_nat_p k Hk) (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
We will prove f w ∈ SNo_recipaux x recip_SNo_pos k 1 ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 0) x (SNoL_pos x) recip_SNo_pos ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 1) x (SNoR x) recip_SNo_pos.
Apply binunionI1 to the current goal.
Apply binunionI2 to the current goal.
We will prove (1 + (u + - x) * w) * recip_SNo_pos u ∈ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 0) x (SNoL_pos x) recip_SNo_pos.
Apply SNo_recipauxset_I (SNo_recipaux x recip_SNo_pos k 0) x (SNoL_pos x) recip_SNo_pos w to the current goal.
We will prove w ∈ SNo_recipaux x recip_SNo_pos k 0.
An exact proof term for the current goal is Hwk.
An exact proof term for the current goal is Hu.
We prove the intermediate claim L6: ∀z ∈ R, f z ∈ L.
Let z be given.
Assume Hz.
Apply LRE z Hz to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume Hzk: z ∈ SNo_recipaux x recip_SNo_pos k 1.
Apply LLI (ordsucc k) (omega_ordsucc k Hk) to the current goal.
We will prove (1 + (u + - x) * z) * recip_SNo_pos u ∈ SNo_recipaux x recip_SNo_pos (ordsucc k) 0.
rewrite the current goal using SNo_recipaux_S x recip_SNo_pos k (omega_nat_p k Hk) (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
We will prove (1 + (u + - x) * z) * recip_SNo_pos u ∈ SNo_recipaux x recip_SNo_pos k 0 ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 0) x (SNoR x) recip_SNo_pos ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 1) x (SNoL_pos x) recip_SNo_pos.
Apply binunionI2 to the current goal.
We will prove (1 + (u + - x) * z) * recip_SNo_pos u ∈ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 1) x (SNoL_pos x) recip_SNo_pos.
Apply SNo_recipauxset_I (SNo_recipaux x recip_SNo_pos k 1) x (SNoL_pos x) recip_SNo_pos z to the current goal.
We will prove z ∈ SNo_recipaux x recip_SNo_pos k 1.
An exact proof term for the current goal is Hzk.
An exact proof term for the current goal is Hu.
We prove the intermediate claim Luu: SNo (u * u).
An exact proof term for the current goal is SNo_mul_SNo u u Hua1 Hua1.
We prove the intermediate claim Luupos: 0 < u * u.
An exact proof term for the current goal is mul_SNo_pos_pos u u Hua1 Hua1 Hub Hub.
We prove the intermediate claim Luun0: u * u ≠ 0.
Assume H.
Apply SNoLt_irref 0 to the current goal.
rewrite the current goal using H (from right to left) at position 2.
An exact proof term for the current goal is Luupos.
We prove the intermediate claim L2u: SNo (2 * u).
An exact proof term for the current goal is SNo_mul_SNo 2 u SNo_2 Hua1.
We prove the intermediate claim Lf: ∀v, SNo v → ∀p : prop, (SNo ((u + - x) * v) → SNo (1 + ((u + - x) * v)) → SNo (f v) → p) → p.
Let v be given.
Assume Hv.
Let p be given.
Assume Hp.
We prove the intermediate claim Lf1: SNo ((u + - x) * v).
Apply SNo_mul_SNo to the current goal.
An exact proof term for the current goal is Lumx.
An exact proof term for the current goal is Hv.
We prove the intermediate claim Lf2: SNo (1 + (u + - x) * v).
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is SNo_1.
An exact proof term for the current goal is Lf1.
We prove the intermediate claim Lf3: SNo ((1 + (u + - x) * v) * recip_SNo_pos u).
Apply SNo_mul_SNo to the current goal.
An exact proof term for the current goal is Lf2.
An exact proof term for the current goal is Lru.
An exact proof term for the current goal is Hp Lf1 Lf2 Lf3.
We prove the intermediate claim Luf: ∀v, SNo v → u * f v = 1 + (u + - x) * v.
Let v be given.
Assume Hv.
Apply Lf v Hv to the current goal.
Assume Humxv: SNo ((u + - x) * v).
Assume H1umxv: SNo (1 + (u + - x) * v).
Assume Hfv: SNo (f v).
We will prove u * ((1 + (u + - x) * v) * recip_SNo_pos u) = 1 + (u + - x) * v.
rewrite the current goal using mul_SNo_com (1 + (u + - x) * v) (recip_SNo_pos u) H1umxv Lru (from left to right).
rewrite the current goal using mul_SNo_assoc u (recip_SNo_pos u) (1 + (u + - x) * v) Hua1 Lru H1umxv (from left to right).
rewrite the current goal using recip_SNo_pos_invR u Hua1 Hub (from left to right).
An exact proof term for the current goal is mul_SNo_oneL (1 + (u + - x) * v) H1umxv.
We prove the intermediate claim L7: ∀v, SNo v → f (f v) = (v * u * u + x * x * v + 2 * u + - ((2 * u) * x * v + x)) :/: (u * u).
Let v be given.
Assume Hv.
Set v' to be the term f v.
Apply Lf v Hv to the current goal.
Assume Humxv: SNo ((u + - x) * v).
Assume H1umxv: SNo (1 + (u + - x) * v).
Assume Hv': SNo v'.
Apply Lf v' Hv' to the current goal.
Assume Humxv': SNo ((u + - x) * v').
Assume H1umxv': SNo (1 + (u + - x) * v').
Assume Hfv': SNo (f v').
We prove the intermediate claim Lxv: SNo (x * v).
An exact proof term for the current goal is SNo_mul_SNo x v Hx Hv.
We prove the intermediate claim Lxxv: SNo (x * x * v).
An exact proof term for the current goal is SNo_mul_SNo x (x * v) Hx Lxv.
We prove the intermediate claim L2uxv: SNo ((2 * u) * x * v).
An exact proof term for the current goal is SNo_mul_SNo (2 * u) (x * v) L2u Lxv.
We prove the intermediate claim Lvuu: SNo (v * u * u).
An exact proof term for the current goal is SNo_mul_SNo v (u * u) Hv Luu.
We prove the intermediate claim Luxv: SNo (u * x * v).
An exact proof term for the current goal is SNo_mul_SNo u (x * v) Hua1 Lxv.
We prove the intermediate claim Luv: SNo (u * v).
An exact proof term for the current goal is SNo_mul_SNo u v Hua1 Hv.
We prove the intermediate claim Lxuv: SNo (x * u * v).
An exact proof term for the current goal is SNo_mul_SNo x (u * v) Hx Luv.
We prove the intermediate claim Lmuxv: SNo (- u * x * v).
An exact proof term for the current goal is SNo_minus_SNo (u * x * v) Luxv.
We prove the intermediate claim Lmxuv: SNo (- x * u * v).
An exact proof term for the current goal is SNo_minus_SNo (x * u * v) Lxuv.
We prove the intermediate claim Lmxmxuv: SNo (- x + - x * u * v).
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Lmx.
An exact proof term for the current goal is Lmxuv.
We prove the intermediate claim Lmxmxuvxxv: SNo (- x + - x * u * v + x * x * v).
Apply SNo_add_SNo_3 to the current goal.
An exact proof term for the current goal is Lmx.
An exact proof term for the current goal is Lmxuv.
An exact proof term for the current goal is Lxxv.
We will prove f v' = (v * u * u + x * x * v + 2 * u + - ((2 * u) * x * v + x)) :/: (u * u).
Use symmetry.
Apply mul_div_SNo_nonzero_eq (v * u * u + x * x * v + 2 * u + - ((2 * u) * x * v + x)) (u * u) (f v') (SNo_add_SNo_4 (v * u * u) (x * x * v) (2 * u) (- ((2 * u) * x * v + x)) Lvuu Lxxv L2u (SNo_minus_SNo ((2 * u) * x * v + x) (SNo_add_SNo ((2 * u) * x * v) x L2uxv Hx))) Luu Hfv' Luun0 to the current goal.
We will prove v * u * u + x * x * v + 2 * u + - ((2 * u) * x * v + x) = (u * u) * f v'.
Use transitivity with u + u * (1 + (u + - x) * v) + - x * (1 + (u + - x) * v), u + u * u * v' + - x * u * v', u * (1 + (u + - x) * v'), and u * (u * f v').
We will prove v * u * u + x * x * v + 2 * u + - ((2 * u) * x * v + x) = u + u * (1 + (u + - x) * v) + - x * (1 + (u + - x) * v).
Use transitivity with v * u * u + u + u + - u * x * v + (- x + - x * u * v + x * x * v), and u + (v * u * u + u + - u * x * v) + (- x + - x * u * v + x * x * v).
We will prove v * u * u + x * x * v + 2 * u + - ((2 * u) * x * v + x) = v * u * u + u + u + - u * x * v + (- x + - x * u * v + x * x * v).
Use f_equal.
We will prove x * x * v + 2 * u + - ((2 * u) * x * v + x) = u + u + - u * x * v + (- x + - x * u * v + x * x * v).
rewrite the current goal using add_SNo_com_3_0_1 (x * x * v) (2 * u) (- ((2 * u) * x * v + x)) Lxxv L2u (SNo_minus_SNo ((2 * u) * x * v + x) (SNo_add_SNo ((2 * u) * x * v) x L2uxv Hx)) (from left to right).
We will prove 2 * u + x * x * v + - ((2 * u) * x * v + x) = u + u + - u * x * v + (- x + - x * u * v + x * x * v).
rewrite the current goal using add_SNo_1_1_2 (from right to left) at position 1.
rewrite the current goal using mul_SNo_distrR 1 1 u SNo_1 SNo_1 Hua1 (from left to right).
rewrite the current goal using mul_SNo_oneL u Hua1 (from left to right).
We will prove (u + u) + x * x * v + - ((2 * u) * x * v + x) = u + u + - u * x * v + (- x + - x * u * v + x * x * v).
Use transitivity with and u + u + x * x * v + - ((2 * u) * x * v + x).
Use symmetry.
Apply add_SNo_assoc u u (x * x * v + - ((2 * u) * x * v + x)) Hua1 Hua1 to the current goal.
We will prove SNo (x * x * v + - ((2 * u) * x * v + x)).
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Lxxv.
Apply SNo_minus_SNo to the current goal.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is L2uxv.
An exact proof term for the current goal is Hx.
Use f_equal.
Use f_equal.
We will prove x * x * v + - ((2 * u) * x * v + x) = - u * x * v + (- x + - x * u * v + x * x * v).
Use transitivity with and x * x * v + - u * x * v + - x + - x * u * v.
We will prove x * x * v + - ((2 * u) * x * v + x) = x * x * v + - u * x * v + - x + - x * u * v.
Use f_equal.
We will prove - ((2 * u) * x * v + x) = - u * x * v + - x + - x * u * v.
rewrite the current goal using minus_add_SNo_distr_3 (u * x * v) x (x * u * v) Luxv Hx Lxuv (from right to left).
We will prove - ((2 * u) * x * v + x) = - (u * x * v + x + x * u * v).
Use f_equal.
We will prove (2 * u) * x * v + x = u * x * v + x + x * u * v.
rewrite the current goal using mul_SNo_com_3_0_1 x u v Hx Hua1 Hv (from left to right).
We will prove (2 * u) * x * v + x = u * x * v + x + u * x * v.
rewrite the current goal using add_SNo_com x (u * x * v) Hx Luxv (from left to right).
rewrite the current goal using add_SNo_assoc (u * x * v) (u * x * v) x Luxv Luxv Hx (from left to right).
Use f_equal.
We will prove (2 * u) * x * v = u * x * v + u * x * v.
rewrite the current goal using add_SNo_1_1_2 (from right to left) at position 1.
rewrite the current goal using mul_SNo_distrR 1 1 u SNo_1 SNo_1 Hua1 (from left to right).
rewrite the current goal using mul_SNo_oneL u Hua1 (from left to right).
We will prove (u + u) * x * v = u * x * v + u * x * v.
An exact proof term for the current goal is mul_SNo_distrR u u (x * v) Hua1 Hua1 Lxv.
We will prove x * x * v + - u * x * v + - x + - x * u * v = - u * x * v + (- x + - x * u * v + x * x * v).
rewrite the current goal using add_SNo_com_3_0_1 (x * x * v) (- u * x * v) (- x + - x * u * v) Lxxv Lmuxv Lmxmxuv (from left to right).
Use f_equal.
We will prove x * x * v + - x + - x * u * v = - x + - x * u * v + x * x * v.
rewrite the current goal using add_SNo_com_3_0_1 (x * x * v) (- x) (- x * u * v) Lxxv Lmx Lmxuv (from left to right).
Use f_equal.
We will prove x * x * v + - x * u * v = - x * u * v + x * x * v.
An exact proof term for the current goal is add_SNo_com (x * x * v) (- x * u * v) Lxxv Lmxuv.
We will prove v * u * u + u + u + - u * x * v + (- x + - x * u * v + x * x * v) = u + (v * u * u + u + - u * x * v) + (- x + - x * u * v + x * x * v).
rewrite the current goal using add_SNo_com_3_0_1 (v * u * u) u (u + - u * x * v + (- x + - x * u * v + x * x * v)) Lvuu Hua1 (from left to right).
We will prove u + v * u * u + u + - u * x * v + (- x + - x * u * v + x * x * v) = u + (v * u * u + u + - u * x * v) + (- x + - x * u * v + x * x * v).
Use f_equal.
We will prove v * u * u + u + - u * x * v + (- x + - x * u * v + x * x * v) = (v * u * u + u + - u * x * v) + (- x + - x * u * v + x * x * v).
Apply add_SNo_assoc_4 to the current goal.
An exact proof term for the current goal is Lvuu.
An exact proof term for the current goal is Hua1.
An exact proof term for the current goal is Lmuxv.
An exact proof term for the current goal is Lmxmxuvxxv.
Apply SNo_add_SNo_3 to the current goal.
An exact proof term for the current goal is Hua1.
An exact proof term for the current goal is Lmuxv.
An exact proof term for the current goal is Lmxmxuvxxv.
We will prove u + (v * u * u + u + - u * x * v) + (- x + - x * u * v + x * x * v) = u + u * (1 + (u + - x) * v) + - x * (1 + (u + - x) * v).
Use f_equal.
Use f_equal.
We will prove v * u * u + u + - u * x * v = u * (1 + (u + - x) * v).
rewrite the current goal using mul_SNo_distrL u 1 ((u + - x) * v) Hua1 SNo_1 Humxv (from left to right).
We will prove v * u * u + u + - u * x * v = u * 1 + u * (u + - x) * v.
rewrite the current goal using mul_SNo_oneR u Hua1 (from left to right).
We will prove v * u * u + u + - u * x * v = u + u * (u + - x) * v.
rewrite the current goal using add_SNo_com_3_0_1 (v * u * u) u (- u * x * v) Lvuu Hua1 (SNo_minus_SNo (u * x * v) Luxv) (from left to right).
We will prove u + v * u * u + - u * x * v = u + u * (u + - x) * v.
Use f_equal.
We will prove v * u * u + - u * x * v = u * (u + - x) * v.
rewrite the current goal using mul_SNo_distrR u (- x) v Hua1 Lmx Hv (from left to right).
We will prove v * u * u + - u * x * v = u * (u * v + (- x) * v).
rewrite the current goal using mul_SNo_distrL u (u * v) ((- x) * v) Hua1 Luv (SNo_mul_SNo (- x) v Lmx Hv) (from left to right).
We will prove v * u * u + - u * x * v = u * u * v + u * (- x) * v.
Use f_equal.
We will prove v * u * u = u * u * v.
rewrite the current goal using mul_SNo_com u v Hua1 Hv (from left to right).
An exact proof term for the current goal is mul_SNo_com_3_0_1 v u u Hv Hua1 Hua1.
We will prove - u * x * v = u * (- x) * v.
rewrite the current goal using mul_SNo_minus_distrL x v Hx Hv (from left to right).
Use symmetry.
An exact proof term for the current goal is mul_SNo_minus_distrR u (x * v) Hua1 Lxv.
We will prove - x + - x * u * v + x * x * v = - x * (1 + (u + - x) * v).
rewrite the current goal using mul_SNo_minus_distrL x (1 + (u + - x) * v) Hx H1umxv (from right to left).
We will prove - x + - x * u * v + x * x * v = (- x) * (1 + (u + - x) * v).
Apply mul_SNo_distrL (- x) 1 ((u + - x) * v) Lmx SNo_1 Humxv (λw z ⇒ - x + - x * u * v + x * x * v = z) to the current goal.
We will prove - x + - x * u * v + x * x * v = (- x) * 1 + (- x) * (u + - x) * v.
rewrite the current goal using mul_SNo_oneR (- x) Lmx (from left to right).
We will prove - x + - x * u * v + x * x * v = - x + (- x) * (u + - x) * v.
Use f_equal.
We will prove - x * u * v + x * x * v = (- x) * (u + - x) * v.
rewrite the current goal using mul_SNo_distrR u (- x) v Hua1 Lmx Hv (from left to right).
rewrite the current goal using mul_SNo_distrL (- x) (u * v) ((- x) * v) Lmx Luv (SNo_mul_SNo (- x) v Lmx Hv) (from left to right).
We will prove - x * u * v + x * x * v = (- x) * u * v + (- x) * (- x) * v.
rewrite the current goal using mul_SNo_minus_distrL x (u * v) Hx Luv (from left to right).
We will prove - x * u * v + x * x * v = - x * u * v + (- x) * (- x) * v.
Use f_equal.
We will prove x * x * v = (- x) * (- x) * v.
rewrite the current goal using mul_SNo_assoc (- x) (- x) v Lmx Lmx Hv (from left to right).
rewrite the current goal using mul_SNo_minus_minus x x Hx Hx (from left to right).
An exact proof term for the current goal is mul_SNo_assoc x x v Hx Hx Hv.
We will prove u + u * (1 + (u + - x) * v) + - x * (1 + (u + - x) * v) = u + u * u * v' + - x * u * v'.
An exact proof term for the current goal is Luf v Hv (λw z ⇒ u + u * w + - x * w = u + u * u * v' + - x * u * v') (λq H ⇒ H).
We will prove u + u * u * v' + - x * u * v' = u * (1 + (u + - x) * v').
Apply mul_SNo_distrL u 1 ((u + - x) * v') Hua1 SNo_1 Humxv' (λw z ⇒ u + u * u * v' + - x * u * v' = z) to the current goal.
We will prove u + u * u * v' + - x * u * v' = u * 1 + u * (u + - x) * v'.
rewrite the current goal using mul_SNo_oneR u Hua1 (from left to right).
Use f_equal.
We will prove u * u * v' + - x * u * v' = u * (u + - x) * v'.
Apply mul_SNo_distrR u (- x) v' Hua1 Lmx Hv' (λw z ⇒ u * u * v' + - x * u * v' = u * z) to the current goal.
We will prove u * u * v' + - x * u * v' = u * (u * v' + (- x) * v').
Apply mul_SNo_distrL u (u * v') ((- x) * v') Hua1 (SNo_mul_SNo u v' Hua1 Hv') (SNo_mul_SNo (- x) v' Lmx Hv') (λw z ⇒ u * u * v' + - x * u * v' = z) to the current goal.
We will prove u * u * v' + - x * u * v' = u * u * v' + u * (- x) * v'.
Use f_equal.
We will prove - x * u * v' = u * (- x) * v'.
Apply mul_SNo_com_3_0_1 u (- x) v' Hua1 Lmx Hv' (λw z ⇒ - x * u * v' = z) to the current goal.
We will prove - x * u * v' = (- x) * u * v'.
Use symmetry.
An exact proof term for the current goal is mul_SNo_minus_distrL x (u * v') Hx (SNo_mul_SNo u v' Hua1 Hv').
Use f_equal.
Use symmetry.
An exact proof term for the current goal is Luf v' Hv'.
An exact proof term for the current goal is mul_SNo_assoc u u (f v') Hua1 Hua1 Hfv'.
We prove the intermediate claim L8: ∀w ∈ L, ∃w' ∈ L, w < w'.
Let w be given.
Assume Hw.
We prove the intermediate claim Lw: SNo w.
Apply real_SNo to the current goal.
An exact proof term for the current goal is LLreal w Hw.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Lw.
We prove the intermediate claim Lxxw: SNo (x * x * w).
An exact proof term for the current goal is SNo_mul_SNo x (x * w) Hx Lxw.
We prove the intermediate claim L2uxw: SNo ((2 * u) * x * w).
An exact proof term for the current goal is SNo_mul_SNo (2 * u) (x * w) L2u Lxw.
We prove the intermediate claim Lwuu: SNo (w * u * u).
An exact proof term for the current goal is SNo_mul_SNo w (u * u) Lw Luu.
We use f (f w) to witness the existential quantifier.
Apply andI to the current goal.
Apply L6 to the current goal.
Apply L5 to the current goal.
An exact proof term for the current goal is Hw.
We will prove w < f (f w).
We prove the intermediate claim L8a: w < (w * u * u + x * x * w + 2 * u + - ((2 * u) * x * w + x)) :/: (u * u).
We will prove w < (w * u * u + x * x * w + 2 * u + - ((2 * u) * x * w + x)) :/: (u * u).
Apply div_SNo_pos_LtR (w * u * u + x * x * w + 2 * u + - ((2 * u) * x * w + x)) (u * u) w to the current goal.
An exact proof term for the current goal is SNo_add_SNo_4 (w * u * u) (x * x * w) (2 * u) (- ((2 * u) * x * w + x)) Lwuu Lxxw L2u (SNo_minus_SNo ((2 * u) * x * w + x) (SNo_add_SNo ((2 * u) * x * w) x L2uxw Hx)).
An exact proof term for the current goal is Luu.
An exact proof term for the current goal is Lw.
We will prove 0 < u * u.
An exact proof term for the current goal is Luupos.
We will prove w * u * u < w * u * u + x * x * w + 2 * u + - ((2 * u) * x * w + x).
rewrite the current goal using add_SNo_0R (w * u * u) (from right to left) at position 1.
We will prove w * u * u + 0 < w * u * u + x * x * w + 2 * u + - ((2 * u) * x * w + x).
Apply add_SNo_Lt2 to the current goal.
An exact proof term for the current goal is Lwuu.
An exact proof term for the current goal is SNo_0.
An exact proof term for the current goal is SNo_add_SNo_3 (x * x * w) (2 * u) (- ((2 * u) * x * w + x)) Lxxw L2u (SNo_minus_SNo ((2 * u) * x * w + x) (SNo_add_SNo ((2 * u) * x * w) x L2uxw Hx)).
We will prove 0 < x * x * w + 2 * u + - ((2 * u) * x * w + x).
Apply add_SNo_minus_Lt2b3 to the current goal.
An exact proof term for the current goal is Lxxw.
An exact proof term for the current goal is L2u.
An exact proof term for the current goal is SNo_add_SNo ((2 * u) * x * w) x L2uxw Hx.
An exact proof term for the current goal is SNo_0.
We will prove 0 + (2 * u) * x * w + x < x * x * w + 2 * u.
rewrite the current goal using add_SNo_0L (from left to right).
We will prove (2 * u) * x * w + x < x * x * w + 2 * u.
rewrite the current goal using add_SNo_com ((2 * u) * x * w) x (SNo_mul_SNo (2 * u) (x * w) L2u Lxw) Hx (from left to right).
rewrite the current goal using add_SNo_com (x * x * w) (2 * u) Lxxw L2u (from left to right).
rewrite the current goal using mul_SNo_oneR x Hx (from right to left) at position 1.
We will prove x * 1 + (2 * u) * x * w < 2 * u + x * x * w.
rewrite the current goal using mul_SNo_oneR (2 * u) L2u (from right to left) at position 2.
We will prove x * 1 + (2 * u) * x * w < (2 * u) * 1 + x * x * w.
Apply mul_SNo_Lt to the current goal.
An exact proof term for the current goal is L2u.
An exact proof term for the current goal is SNo_1.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Lxw.
We will prove x < 2 * u.
An exact proof term for the current goal is H3.
We will prove x * w < 1.
rewrite the current goal using mul_SNo_com x w Hx Lw (from left to right).
Apply div_SNo_pos_LtR' to the current goal.
An exact proof term for the current goal is SNo_1.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Lw.
We will prove 0 < x.
An exact proof term for the current goal is Hxpos.
We will prove w < 1 :/: x.
We will prove w < 1 * recip_SNo x.
rewrite the current goal using mul_SNo_oneL (recip_SNo x) (SNo_recip_SNo x Hx) (from left to right).
rewrite the current goal using recip_SNo_poscase x Hxpos (from left to right).
We will prove w < recip_SNo_pos x.
rewrite the current goal using LrxLR (from left to right).
We will prove w < y.
Apply HLR3 to the current goal.
An exact proof term for the current goal is Hw.
An exact proof term for the current goal is SNo_add_SNo ((2 * u) * x * w) x (SNo_mul_SNo (2 * u) (x * w) L2u Lxw) Hx.
An exact proof term for the current goal is Lwuu.
An exact proof term for the current goal is L7 w Lw (λu v ⇒ w < v) L8a.
We prove the intermediate claim L9: ∀z ∈ R, ∃z' ∈ R, z' < z.
Let z be given.
Assume Hz.
We prove the intermediate claim Lz: SNo z.
Apply real_SNo to the current goal.
An exact proof term for the current goal is LRreal z Hz.
We prove the intermediate claim Lxz: SNo (x * z).
An exact proof term for the current goal is SNo_mul_SNo x z Hx Lz.
We prove the intermediate claim Lxxz: SNo (x * x * z).
An exact proof term for the current goal is SNo_mul_SNo x (x * z) Hx Lxz.
We prove the intermediate claim L2uxz: SNo ((2 * u) * x * z).
An exact proof term for the current goal is SNo_mul_SNo (2 * u) (x * z) L2u Lxz.
We prove the intermediate claim Lzuu: SNo (z * u * u).
An exact proof term for the current goal is SNo_mul_SNo z (u * u) Lz Luu.
We use f (f z) to witness the existential quantifier.
Apply andI to the current goal.
Apply L5 to the current goal.
Apply L6 to the current goal.
An exact proof term for the current goal is Hz.
We will prove f (f z) < z.
We prove the intermediate claim L9a: (z * u * u + x * x * z + 2 * u + - ((2 * u) * x * z + x)) :/: (u * u) < z.
Apply div_SNo_pos_LtL (z * u * u + x * x * z + 2 * u + - ((2 * u) * x * z + x)) (u * u) z to the current goal.
An exact proof term for the current goal is SNo_add_SNo_4 (z * u * u) (x * x * z) (2 * u) (- ((2 * u) * x * z + x)) Lzuu Lxxz L2u (SNo_minus_SNo ((2 * u) * x * z + x) (SNo_add_SNo ((2 * u) * x * z) x L2uxz Hx)).
An exact proof term for the current goal is Luu.
An exact proof term for the current goal is Lz.
We will prove 0 < u * u.
An exact proof term for the current goal is Luupos.
We will prove z * u * u + x * x * z + 2 * u + - ((2 * u) * x * z + x) < z * u * u.
rewrite the current goal using add_SNo_0R (z * u * u) (from right to left) at position 2.
We will prove z * u * u + x * x * z + 2 * u + - ((2 * u) * x * z + x) < z * u * u + 0.
Apply add_SNo_Lt2 to the current goal.
An exact proof term for the current goal is Lzuu.
An exact proof term for the current goal is SNo_add_SNo_3 (x * x * z) (2 * u) (- ((2 * u) * x * z + x)) Lxxz L2u (SNo_minus_SNo ((2 * u) * x * z + x) (SNo_add_SNo ((2 * u) * x * z) x L2uxz Hx)).
An exact proof term for the current goal is SNo_0.
We will prove x * x * z + 2 * u + - ((2 * u) * x * z + x) < 0.
Apply add_SNo_minus_Lt1b3 to the current goal.
An exact proof term for the current goal is Lxxz.
An exact proof term for the current goal is L2u.
An exact proof term for the current goal is SNo_add_SNo ((2 * u) * x * z) x L2uxz Hx.
An exact proof term for the current goal is SNo_0.
We will prove x * x * z + 2 * u < 0 + (2 * u) * x * z + x.
rewrite the current goal using add_SNo_0L (from left to right).
We will prove x * x * z + 2 * u < (2 * u) * x * z + x.
rewrite the current goal using mul_SNo_oneR x Hx (from right to left) at position 4.
We will prove x * x * z + 2 * u < (2 * u) * x * z + x * 1.
rewrite the current goal using mul_SNo_oneR (2 * u) L2u (from right to left) at position 1.
We will prove x * x * z + (2 * u) * 1 < (2 * u) * x * z + x * 1.
Apply mul_SNo_Lt to the current goal.
An exact proof term for the current goal is L2u.
An exact proof term for the current goal is Lxz.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is SNo_1.
We will prove x < 2 * u.
An exact proof term for the current goal is H3.
We will prove 1 < x * z.
rewrite the current goal using mul_SNo_com x z Hx Lz (from left to right).
We will prove 1 < z * x.
Apply div_SNo_pos_LtL' to the current goal.
An exact proof term for the current goal is SNo_1.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Lz.
We will prove 0 < x.
An exact proof term for the current goal is Hxpos.
We will prove 1 :/: x < z.
We will prove 1 * recip_SNo x < z.
rewrite the current goal using mul_SNo_oneL (recip_SNo x) (SNo_recip_SNo x Hx) (from left to right).
rewrite the current goal using recip_SNo_poscase x Hxpos (from left to right).
We will prove recip_SNo_pos x < z.
rewrite the current goal using LrxLR (from left to right).
We will prove y < z.
Apply HLR4 to the current goal.
An exact proof term for the current goal is Hz.
An exact proof term for the current goal is SNo_add_SNo ((2 * u) * x * z) x (SNo_mul_SNo (2 * u) (x * z) L2u Lxz) Hx.
An exact proof term for the current goal is Lzuu.
An exact proof term for the current goal is L7 z Lz (λu v ⇒ v < z) L9a.
We will prove recip_SNo_pos x ∈ real.
rewrite the current goal using recip_SNo_pos_eq x Hx (from left to right).
We will prove SNoCut L R ∈ real.
Apply real_SNoCut to the current goal.
An exact proof term for the current goal is LLreal.
An exact proof term for the current goal is LRreal.
An exact proof term for the current goal is LLR.
An exact proof term for the current goal is LL0.
We will prove R ≠ 0.
Assume H4: R = 0.
Apply EmptyE ((1 + (u + - x) * 0) * recip_SNo_pos u) to the current goal.
We will prove (1 + (u + - x) * 0) * recip_SNo_pos u ∈ 0.
rewrite the current goal using H4 (from right to left) at position 3.
We will prove (1 + (u + - x) * 0) * recip_SNo_pos u ∈ R.
Apply L5 0 to the current goal.
We will prove 0 ∈ L.
Apply LLI 0 (nat_p_omega 0 nat_0) to the current goal.
We will prove 0 ∈ SNo_recipaux x recip_SNo_pos 0 0.
rewrite the current goal using SNo_recipaux_0 x recip_SNo_pos (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
We will prove 0 ∈ {0}.
Apply SingI to the current goal.
We will prove ∀w ∈ L, ∃w' ∈ L, w < w'.
An exact proof term for the current goal is L8.
We will prove ∀z ∈ R, ∃z' ∈ R, z' < z.
An exact proof term for the current goal is L9.
An exact proof term for the current goal is L2.
∎