Let x be given.
Assume Hx.
Let p be given.
Assume Hp.
Apply real_E x Hx to the current goal.
Assume Hx1 Hx2 Hx3 _ _ Hx4 Hx5.
Apply SNo_prereal_incr_lower_approx x Hx1 Hx4 Hx5 to the current goal.
Let f be given.
Assume Hf.
Apply Hf to the current goal.
Assume Hf1 Hf2.
Apply SNo_prereal_decr_upper_approx x Hx1 Hx4 Hx5 to the current goal.
Let g be given.
Assume Hg.
Apply Hg to the current goal.
Assume Hg1 Hg2.
We prove the intermediate claim Lf: ∀n ∈ ω, SNo (f n).
Let n be given.
Assume Hn.
Apply SNoS_E2 ω omega_ordinal (f n) (ap_Pi ω (λ_ ⇒ SNoS_ ω) f n Hf1 Hn) to the current goal.
Assume _ _ H _.
An exact proof term for the current goal is H.
We prove the intermediate claim Lg: ∀n ∈ ω, SNo (g n).
Let n be given.
Assume Hn.
Apply SNoS_E2 ω omega_ordinal (g n) (ap_Pi ω (λ_ ⇒ SNoS_ ω) g n Hg1 Hn) to the current goal.
Assume _ _ H _.
An exact proof term for the current goal is H.
We prove the intermediate claim Lf1: ∀n ∈ ω, f n < x.
Let n be given.
Assume Hn.
Apply Hf2 n Hn to the current goal.
Assume H _.
Apply H to the current goal.
Assume H _.
An exact proof term for the current goal is H.
We prove the intermediate claim Lf2: ∀n ∈ ω, x < f n + eps_ n.
Let n be given.
Assume Hn.
Apply Hf2 n Hn to the current goal.
Assume H _.
Apply H to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
We prove the intermediate claim Lf3: ∀n ∈ ω, ∀i ∈ n, f i < f n.
Let n be given.
Assume Hn.
Apply Hf2 n Hn to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
We prove the intermediate claim Lg1: ∀n ∈ ω, g n + - eps_ n < x.
Let n be given.
Assume Hn.
Apply Hg2 n Hn to the current goal.
Assume H _.
Apply H to the current goal.
Assume H _.
An exact proof term for the current goal is H.
We prove the intermediate claim Lg2: ∀n ∈ ω, x < g n.
Let n be given.
Assume Hn.
Apply Hg2 n Hn to the current goal.
Assume H _.
Apply H to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
We prove the intermediate claim Lg3: ∀n ∈ ω, ∀i ∈ n, g n < g i.
Let n be given.
Assume Hn.
Apply Hg2 n Hn to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
We prove the intermediate claim Lfg: ∀n m ∈ ω, f n < g m.
Let n be given.
Assume Hn.
Let m be given.
Assume Hm.
Apply SNoLt_tra (f n) x (g m) (Lf n Hn) Hx1 (Lg m Hm) to the current goal.
We will prove f n < x.
An exact proof term for the current goal is Lf1 n Hn.
We will prove x < g m.
An exact proof term for the current goal is Lg2 m Hm.
Set L to be the term {f n|n ∈ ω}.
Set R to be the term {g n|n ∈ ω}.
Apply SNo_approx_real_lem f Hf1 g Hg1 Lfg to the current goal.
Assume H1: SNoCutP L R.
Assume H2: SNo (SNoCut L R).
Assume H3: SNoLev (SNoCut L R) ∈ ordsucc ω.
Assume H4: SNoCut L R ∈ SNoS_ (ordsucc ω).
Assume H5: ∀n ∈ ω, f n < SNoCut L R.
Assume H6: ∀n ∈ ω, SNoCut L R < g n.
We prove the intermediate claim Lxfg: x = SNoCut L R.
rewrite the current goal using SNo_eta x Hx1 (from left to right).
Apply SNoCut_ext (SNoL x) (SNoR x) L R (SNoCutP_SNoL_SNoR x Hx1) H1 to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL x.
We will prove w < SNoCut L R.
Apply SNoL_E x Hx1 w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev x.
Assume Hw3: w < x.
We prove the intermediate claim Lw1: w ∈ SNoS_ ω.
An exact proof term for the current goal is SNoLev_In_real_SNoS_omega x Hx w Hw1 Hw2.
We prove the intermediate claim Lw2: 0 < x + - w.
An exact proof term for the current goal is SNoLt_minus_pos w x Hw1 Hx1 Hw3.
We prove the intermediate claim Lw3: ∃k ∈ ω, w + eps_ k ≤ x.
Apply dneg to the current goal.
Assume H7: ¬ ∃k ∈ ω, w + eps_ k ≤ x.
We prove the intermediate claim Lw3a: w = x.
Apply Hx4 w Lw1 to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
We will prove abs_SNo (w + - x) < eps_ k.
rewrite the current goal using abs_SNo_dist_swap w x Hw1 Hx1 (from left to right).
We will prove abs_SNo (x + - w) < eps_ k.
rewrite the current goal using pos_abs_SNo (x + - w) Lw2 (from left to right).
We will prove x + - w < eps_ k.
Apply SNoLtLe_or (x + - w) (eps_ k) (SNo_add_SNo x (- w) Hx1 (SNo_minus_SNo w Hw1)) (SNo_eps_ k Hk) to the current goal.
Assume H8: x + - w < eps_ k.
An exact proof term for the current goal is H8.
Assume H8: eps_ k ≤ x + - w.
We will prove False.
Apply H7 to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk.
We will prove w + eps_ k ≤ x.
rewrite the current goal using add_SNo_minus_R2' x w Hx1 Hw1 (from right to left).
We will prove w + eps_ k ≤ (x + - w) + w.
rewrite the current goal using add_SNo_com w (eps_ k) Hw1 (SNo_eps_ k Hk) (from left to right).
We will prove eps_ k + w ≤ (x + - w) + w.
An exact proof term for the current goal is add_SNo_Le1 (eps_ k) w (x + - w) (SNo_eps_ k Hk) Hw1 (SNo_add_SNo x (- w) Hx1 (SNo_minus_SNo w Hw1)) H8.
Apply SNoLt_irref x to the current goal.
rewrite the current goal using Lw3a (from right to left) at position 1.
An exact proof term for the current goal is Hw3.
Apply Lw3 to the current goal.
Let k be given.
Assume Hk.
Apply Hk to the current goal.
Assume Hk1: k ∈ ω.
Assume Hk2: w + eps_ k ≤ x.
We will prove w < SNoCut L R.
Apply SNoLt_tra w (f k) (SNoCut L R) Hw1 (Lf k Hk1) H2 to the current goal.
We will prove w < f k.
Apply add_SNo_Lt1_cancel w (eps_ k) (f k) Hw1 (SNo_eps_ k Hk1) (Lf k Hk1) to the current goal.
We will prove w + eps_ k < f k + eps_ k.
Apply SNoLeLt_tra (w + eps_ k) x (f k + eps_ k) (SNo_add_SNo w (eps_ k) Hw1 (SNo_eps_ k Hk1)) Hx1 (SNo_add_SNo (f k) (eps_ k) (Lf k Hk1) (SNo_eps_ k Hk1)) Hk2 to the current goal.
We will prove x < f k + eps_ k.
Apply Hf2 k Hk1 to the current goal.
Assume H _.
Apply H to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
We will prove f k < SNoCut L R.
An exact proof term for the current goal is H5 k Hk1.
Let z be given.
Assume Hz: z ∈ SNoR x.
We will prove SNoCut L R < z.
Apply SNoR_E x Hx1 z Hz to the current goal.
Assume Hz1: SNo z.
Assume Hz2: SNoLev z ∈ SNoLev x.
Assume Hz3: x < z.
We prove the intermediate claim Lz1: z ∈ SNoS_ ω.
An exact proof term for the current goal is SNoLev_In_real_SNoS_omega x Hx z Hz1 Hz2.
We prove the intermediate claim Lz2: 0 < z + - x.
An exact proof term for the current goal is SNoLt_minus_pos x z Hx1 Hz1 Hz3.
We prove the intermediate claim Lz3: ∃k ∈ ω, x + eps_ k ≤ z.
Apply dneg to the current goal.
Assume H7: ¬ ∃k ∈ ω, x + eps_ k ≤ z.
We prove the intermediate claim Lz3a: z = x.
Apply Hx4 z Lz1 to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
We will prove abs_SNo (z + - x) < eps_ k.
rewrite the current goal using pos_abs_SNo (z + - x) Lz2 (from left to right).
We will prove z + - x < eps_ k.
Apply SNoLtLe_or (z + - x) (eps_ k) (SNo_add_SNo z (- x) Hz1 (SNo_minus_SNo x Hx1)) (SNo_eps_ k Hk) to the current goal.
Assume H8: z + - x < eps_ k.
An exact proof term for the current goal is H8.
Assume H8: eps_ k ≤ z + - x.
We will prove False.
Apply H7 to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk.
We will prove x + eps_ k ≤ z.
rewrite the current goal using add_SNo_minus_R2' z x Hz1 Hx1 (from right to left).
We will prove x + eps_ k ≤ (z + - x) + x.
rewrite the current goal using add_SNo_com x (eps_ k) Hx1 (SNo_eps_ k Hk) (from left to right).
We will prove eps_ k + x ≤ (z + - x) + x.
An exact proof term for the current goal is add_SNo_Le1 (eps_ k) x (z + - x) (SNo_eps_ k Hk) Hx1 (SNo_add_SNo z (- x) Hz1 (SNo_minus_SNo x Hx1)) H8.
Apply SNoLt_irref x to the current goal.
rewrite the current goal using Lz3a (from right to left) at position 2.
An exact proof term for the current goal is Hz3.
Apply Lz3 to the current goal.
Let k be given.
Assume Hk.
Apply Hk to the current goal.
Assume Hk1: k ∈ ω.
Assume Hk2: x + eps_ k ≤ z.
We will prove SNoCut L R < z.
Apply SNoLt_tra (SNoCut L R) (g k) z H2 (Lg k Hk1) Hz1 to the current goal.
An exact proof term for the current goal is H6 k Hk1.
We will prove g k < z.
Apply SNoLtLe_tra (g k) (x + eps_ k) z (Lg k Hk1) (SNo_add_SNo x (eps_ k) Hx1 (SNo_eps_ k Hk1)) Hz1 to the current goal.
We will prove g k < x + eps_ k.
Apply add_SNo_minus_Lt1 (g k) (eps_ k) x (Lg k Hk1) (SNo_eps_ k Hk1) Hx1 to the current goal.
We will prove g k + - eps_ k < x.
An exact proof term for the current goal is Lg1 k Hk1.
We will prove x + eps_ k ≤ z.
An exact proof term for the current goal is Hk2.
Let w be given.
Assume Hw: w ∈ L.
rewrite the current goal using SNo_eta x Hx1 (from right to left).
We will prove w < x.
Apply ReplE_impred ω (λn ⇒ f n) w Hw to the current goal.
Let n be given.
Assume Hn.
Assume Hwn: w = f n.
rewrite the current goal using Hwn (from left to right).
We will prove f n < x.
An exact proof term for the current goal is Lf1 n Hn.
Let z be given.
Assume Hz: z ∈ R.
rewrite the current goal using SNo_eta x Hx1 (from right to left).
We will prove x < z.
Apply ReplE_impred ω (λn ⇒ g n) z Hz to the current goal.
Let m be given.
Assume Hm.
Assume Hzm: z = g m.
rewrite the current goal using Hzm (from left to right).
We will prove x < g m.
An exact proof term for the current goal is Lg2 m Hm.
An exact proof term for the current goal is Hp f Hf1 g Hg1 Lf1 Lf2 Lf3 Lg1 Lg2 Lg3 H1 Lxfg.
∎