Let x be given.
Assume Hx.
Let f be given.
Assume Hf1.
Let g be given.
Assume Hg1 Hf2 Hf3 Hf4 Hg3 Hg4.
Set L to be the term {f n|n ∈ ω}.
Set R to be the term {g n|n ∈ ω}.
Assume Hxfg: x = SNoCut L R.
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 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 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) Hx (Lg m Hm) to the current goal.
An exact proof term for the current goal is Hf2 n Hn.
An exact proof term for the current goal is Hg3 m Hm.
Apply SNo_approx_real_lem f Hf1 g Hg1 Lfg to the current goal.
rewrite the current goal using Hxfg (from right to left).
Assume H1: SNoCutP L R.
Assume H2: SNo x.
rewrite the current goal using Hxfg (from right to left).
Assume H3: SNoLev x ∈ ordsucc ω.
rewrite the current goal using Hxfg (from right to left).
Assume H4: x ∈ SNoS_ (ordsucc ω).
rewrite the current goal using Hxfg (from right to left).
Assume H5: ∀n ∈ ω, f n < x.
rewrite the current goal using Hxfg (from right to left).
Assume H6: ∀n ∈ ω, x < g n.
Apply SNoCutP_SNoCut_impred L R H1 to the current goal.
Assume _ _ _ _.
Assume H7: ∀z, SNo z → (∀w ∈ L, w < z) → (∀y ∈ R, z < y) → SNoLev (SNoCut L R) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z.
Apply ordsuccE ω (SNoLev x) H3 to the current goal.
Assume H8: SNoLev x ∈ ω.
Apply SNoS_omega_real to the current goal.
We will prove x ∈ SNoS_ ω.
Apply SNoS_I ω omega_ordinal x (SNoLev x) H8 to the current goal.
We will prove SNo_ (SNoLev x) x.
An exact proof term for the current goal is SNoLev_ x Hx.
Assume H8: SNoLev x = ω.
Apply real_I to the current goal.
We will prove x ∈ SNoS_ (ordsucc ω).
An exact proof term for the current goal is H4.
We will prove x ≠ ω.
Assume H9: x = ω.
We prove the intermediate claim Lbd1: x < g 0.
An exact proof term for the current goal is Hg3 0 (nat_p_omega 0 nat_0).
Apply real_E (g 0) (SNoS_omega_real (g 0) (ap_Pi ω (λ_ ⇒ SNoS_ ω) g 0 Hg1 (nat_p_omega 0 nat_0))) to the current goal.
Assume Hg0a: SNo (g 0).
Assume _ _ _.
Assume Hg0b: g 0 < ω.
Assume _ _.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
Apply SNoLt_tra x (g 0) x Hx Hg0a Hx Lbd1 to the current goal.
We will prove g 0 < x.
rewrite the current goal using H9 (from left to right).
We will prove g 0 < ω.
An exact proof term for the current goal is Hg0b.
We will prove x ≠ - ω.
Assume H9: x = - ω.
We prove the intermediate claim Lbd2: f 0 < x.
An exact proof term for the current goal is Hf2 0 (nat_p_omega 0 nat_0).
Apply real_E (f 0) (SNoS_omega_real (f 0) (ap_Pi ω (λ_ ⇒ SNoS_ ω) f 0 Hf1 (nat_p_omega 0 nat_0))) to the current goal.
Assume Hf0a: SNo (f 0).
Assume _ _.
Assume Hf0b: - ω < f 0.
Assume _ _ _.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
Apply SNoLt_tra x (f 0) x Hx Hf0a Hx to the current goal.
We will prove x < f 0.
rewrite the current goal using H9 (from left to right).
An exact proof term for the current goal is Hf0b.
We will prove f 0 < x.
An exact proof term for the current goal is Lbd2.
We will prove ∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x.
Let q be given.
Assume Hq1 Hq2.
We will prove q = x.
Apply SNoS_E2 ω omega_ordinal q Hq1 to the current goal.
Assume Hq1a Hq1b Hq1c Hq1d.
We prove the intermediate claim Lmq: SNo (- q).
An exact proof term for the current goal is SNo_minus_SNo q Hq1c.
We prove the intermediate claim Lxmq: SNo (x + - q).
An exact proof term for the current goal is SNo_add_SNo x (- q) Hx Lmq.
We prove the intermediate claim Lqmx: SNo (q + - x).
An exact proof term for the current goal is SNo_add_SNo q (- x) Hq1c Lmx.
We prove the intermediate claim L5: ∀w ∈ L, w < q.
Let w be given.
Assume Hw.
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 < q.
Apply SNoLtLe_or (f n) q (Lf n Hn) Hq1c to the current goal.
Assume H9: f n < q.
An exact proof term for the current goal is H9.
Assume H9: q ≤ f n.
Apply real_E (f (ordsucc n)) (SNoS_omega_real (f (ordsucc n)) (ap_Pi ω (λ_ ⇒ SNoS_ ω) f (ordsucc n) Hf1 (omega_ordsucc n Hn))) to the current goal.
Assume _ _ _ _ _.
Assume Hfn2: ∀q' ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q' + - f (ordsucc n)) < eps_ k) → q' = f (ordsucc n).
Assume _.
We prove the intermediate claim L5a: SNo (f (ordsucc n)).
An exact proof term for the current goal is Lf (ordsucc n) (omega_ordsucc n Hn).
We prove the intermediate claim L5b: q < f (ordsucc n).
Apply SNoLeLt_tra q (f n) (f (ordsucc n)) Hq1c (Lf n Hn) L5a H9 to the current goal.
We will prove f n < f (ordsucc n).
Apply Hf4 (ordsucc n) (omega_ordsucc n Hn) to the current goal.
We will prove n ∈ ordsucc n.
Apply ordsuccI2 to the current goal.
We prove the intermediate claim L5c: 0 < f (ordsucc n) + - q.
An exact proof term for the current goal is SNoLt_minus_pos q (f (ordsucc n)) Hq1c L5a L5b.
We prove the intermediate claim L5d: SNo (f (ordsucc n) + - q).
An exact proof term for the current goal is SNo_add_SNo (f (ordsucc n)) (- q) L5a Lmq.
We prove the intermediate claim L5e: f (ordsucc n) < x.
An exact proof term for the current goal is Hf2 (ordsucc n) (omega_ordsucc n Hn).
We prove the intermediate claim L5f: q < x.
An exact proof term for the current goal is SNoLt_tra q (f (ordsucc n)) x Hq1c L5a Hx L5b L5e.
We prove the intermediate claim L5g: 0 < x + - q.
An exact proof term for the current goal is SNoLt_minus_pos q x Hq1c Hx L5f.
We prove the intermediate claim L5h: abs_SNo (q + - x) = x + - q.
rewrite the current goal using abs_SNo_dist_swap q x Hq1c Hx (from left to right).
An exact proof term for the current goal is pos_abs_SNo (x + - q) L5g.
We prove the intermediate claim L5i: q = f (ordsucc n).
Apply Hfn2 q Hq1 to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
We will prove abs_SNo (q + - f (ordsucc n)) < eps_ k.
rewrite the current goal using abs_SNo_dist_swap q (f (ordsucc n)) Hq1c (Lf (ordsucc n) (omega_ordsucc n Hn)) (from left to right).
We will prove abs_SNo (f (ordsucc n) + - q) < eps_ k.
rewrite the current goal using pos_abs_SNo (f (ordsucc n) + - q) L5c (from left to right).
We will prove f (ordsucc n) + - q < eps_ k.
Apply SNoLt_tra (f (ordsucc n) + - q) (x + - q) (eps_ k) L5d Lxmq (SNo_eps_ k Hk) to the current goal.
We will prove f (ordsucc n) + - q < x + - q.
Apply add_SNo_Lt1 (f (ordsucc n)) (- q) x L5a Lmq Hx to the current goal.
We will prove f (ordsucc n) < x.
An exact proof term for the current goal is L5e.
We will prove x + - q < eps_ k.
rewrite the current goal using L5h (from right to left).
We will prove abs_SNo (q + - x) < eps_ k.
An exact proof term for the current goal is Hq2 k Hk.
Apply SNoLt_irref q to the current goal.
rewrite the current goal using L5i (from left to right) at position 2.
An exact proof term for the current goal is L5b.
We prove the intermediate claim L6: ∀z ∈ R, q < z.
Let z be given.
Assume Hz: z ∈ R.
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 q < g m.
Apply SNoLtLe_or q (g m) Hq1c (Lg m Hm) to the current goal.
Assume H9: q < g m.
An exact proof term for the current goal is H9.
Assume H9: g m ≤ q.
Apply real_E (g (ordsucc m)) (SNoS_omega_real (g (ordsucc m)) (ap_Pi ω (λ_ ⇒ SNoS_ ω) g (ordsucc m) Hg1 (omega_ordsucc m Hm))) to the current goal.
Assume _ _ _ _ _.
Assume Hgm2: ∀q' ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q' + - g (ordsucc m)) < eps_ k) → q' = g (ordsucc m).
Assume _.
We prove the intermediate claim L6a: SNo (g (ordsucc m)).
An exact proof term for the current goal is Lg (ordsucc m) (omega_ordsucc m Hm).
We prove the intermediate claim L6b: g (ordsucc m) < q.
Apply SNoLtLe_tra (g (ordsucc m)) (g m) q L6a (Lg m Hm) Hq1c to the current goal.
We will prove g (ordsucc m) < g m.
Apply Hg4 (ordsucc m) (omega_ordsucc m Hm) to the current goal.
We will prove m ∈ ordsucc m.
Apply ordsuccI2 to the current goal.
An exact proof term for the current goal is H9.
We prove the intermediate claim L6c: 0 < q + - g (ordsucc m).
An exact proof term for the current goal is SNoLt_minus_pos (g (ordsucc m)) q L6a Hq1c L6b.
We prove the intermediate claim L6d: SNo (q + - g (ordsucc m)).
An exact proof term for the current goal is SNo_add_SNo q (- g (ordsucc m)) Hq1c (SNo_minus_SNo (g (ordsucc m)) L6a).
We prove the intermediate claim L6e: x < g (ordsucc m).
An exact proof term for the current goal is Hg3 (ordsucc m) (omega_ordsucc m Hm).
We prove the intermediate claim L6f: x < q.
An exact proof term for the current goal is SNoLt_tra x (g (ordsucc m)) q Hx L6a Hq1c L6e L6b.
We prove the intermediate claim L6g: 0 < q + - x.
An exact proof term for the current goal is SNoLt_minus_pos x q Hx Hq1c L6f.
We prove the intermediate claim L6h: abs_SNo (q + - x) = q + - x.
An exact proof term for the current goal is pos_abs_SNo (q + - x) L6g.
We prove the intermediate claim L6i: q = g (ordsucc m).
Apply Hgm2 q Hq1 to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
We will prove abs_SNo (q + - g (ordsucc m)) < eps_ k.
rewrite the current goal using pos_abs_SNo (q + - g (ordsucc m)) L6c (from left to right).
We will prove q + - g (ordsucc m) < eps_ k.
Apply SNoLt_tra (q + - g (ordsucc m)) (q + - x) (eps_ k) L6d Lqmx (SNo_eps_ k Hk) to the current goal.
We will prove q + - g (ordsucc m) < q + - x.
Apply add_SNo_Lt2 q (- g (ordsucc m)) (- x) Hq1c (SNo_minus_SNo (g (ordsucc m)) L6a) Lmx to the current goal.
We will prove - g (ordsucc m) < - x.
Apply minus_SNo_Lt_contra x (g (ordsucc m)) Hx L6a to the current goal.
An exact proof term for the current goal is L6e.
We will prove q + - x < eps_ k.
rewrite the current goal using L6h (from right to left).
We will prove abs_SNo (q + - x) < eps_ k.
An exact proof term for the current goal is Hq2 k Hk.
Apply SNoLt_irref q to the current goal.
rewrite the current goal using L6i (from left to right) at position 1.
An exact proof term for the current goal is L6b.
Apply H7 q Hq1c L5 L6 to the current goal.
rewrite the current goal using Hxfg (from right to left).
rewrite the current goal using H8 (from left to right).
Assume H9: ω ⊆ SNoLev q.
We will prove False.
Apply In_irref (SNoLev q) to the current goal.
We will prove SNoLev q ∈ SNoLev q.
Apply H9 to the current goal.
We will prove SNoLev q ∈ ω.
An exact proof term for the current goal is Hq1a.
∎