Let a be given.
Assume Ha.
Let b be given.
Assume Hb H1.
Apply dneg to the current goal.
Assume HC: ¬ (∃x ∈ real, ∀n ∈ ω, a n ≤ x ∧ x ≤ b n).
We will prove False.
We prove the intermediate claim La1: ∀n ∈ ω, SNo (a n).
Let n be given.
Assume Hn.
Apply real_E (a n) (ap_Pi ω (λ_ ⇒ real) a n Ha Hn) to the current goal.
Assume H _ _ _ _ _ _.
An exact proof term for the current goal is H.
We prove the intermediate claim Lb1: ∀n ∈ ω, SNo (b n).
Let n be given.
Assume Hn.
Apply real_E (b n) (ap_Pi ω (λ_ ⇒ real) b n Hb Hn) to the current goal.
Assume H _ _ _ _ _ _.
An exact proof term for the current goal is H.
We prove the intermediate claim La2: ∀n, nat_p n → ∀m ∈ n, a m ≤ a n.
Apply nat_ind to the current goal.
Let m be given.
Assume Hm: m ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE m Hm.
Let n be given.
Assume Hn.
Assume IHn: ∀m ∈ n, a m ≤ a n.
Let m be given.
Assume Hm: m ∈ ordsucc n.
We will prove a m ≤ a (ordsucc n).
We prove the intermediate claim Ln: n ∈ ω.
An exact proof term for the current goal is nat_p_omega n Hn.
We prove the intermediate claim LSn: ordsucc n ∈ ω.
An exact proof term for the current goal is omega_ordsucc n Ln.
We prove the intermediate claim Lm: m ∈ ω.
An exact proof term for the current goal is omega_TransSet (ordsucc n) LSn m Hm.
We prove the intermediate claim LanSn: a n ≤ a (ordsucc n).
Apply H1 n Ln to the current goal.
Assume H _.
Apply H to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
Apply ordsuccE n m Hm to the current goal.
Assume H2: m ∈ n.
Apply SNoLe_tra (a m) (a n) (a (ordsucc n)) (La1 m Lm) (La1 n Ln) (La1 (ordsucc n) LSn) to the current goal.
We will prove a m ≤ a n.
An exact proof term for the current goal is IHn m H2.
An exact proof term for the current goal is LanSn.
Assume H2: m = n.
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is LanSn.
We prove the intermediate claim Lb2: ∀n, nat_p n → ∀m ∈ n, b n ≤ b m.
Apply nat_ind to the current goal.
Let m be given.
Assume Hm: m ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE m Hm.
Let n be given.
Assume Hn.
Assume IHn: ∀m ∈ n, b n ≤ b m.
Let m be given.
Assume Hm: m ∈ ordsucc n.
We will prove b (ordsucc n) ≤ b m.
We prove the intermediate claim Ln: n ∈ ω.
An exact proof term for the current goal is nat_p_omega n Hn.
We prove the intermediate claim LSn: ordsucc n ∈ ω.
An exact proof term for the current goal is omega_ordsucc n Ln.
We prove the intermediate claim Lm: m ∈ ω.
An exact proof term for the current goal is omega_TransSet (ordsucc n) LSn m Hm.
We prove the intermediate claim LbSnn: b (ordsucc n) ≤ b n.
Apply H1 n Ln to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
Apply ordsuccE n m Hm to the current goal.
Assume H2: m ∈ n.
Apply SNoLe_tra (b (ordsucc n)) (b n) (b m) (Lb1 (ordsucc n) LSn) (Lb1 n Ln) (Lb1 m Lm) to the current goal.
An exact proof term for the current goal is LbSnn.
We will prove b n ≤ b m.
An exact proof term for the current goal is IHn m H2.
Assume H2: m = n.
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is LbSnn.
We prove the intermediate claim Lab: ∀n m ∈ ω, a n ≤ b m.
Let n be given.
Assume Hn.
Let m be given.
Assume Hm.
We prove the intermediate claim Ln: nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn.
We prove the intermediate claim Lm: nat_p m.
An exact proof term for the current goal is omega_nat_p m Hm.
We prove the intermediate claim Labn: a n ≤ b n.
Apply H1 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.
Apply ordinal_trichotomy_or_impred n m (nat_p_ordinal n Ln) (nat_p_ordinal m Lm) to the current goal.
Assume H2: n ∈ m.
We will prove a n ≤ b m.
Apply SNoLe_tra (a n) (a m) (b m) (La1 n Hn) (La1 m Hm) (Lb1 m Hm) to the current goal.
We will prove a n ≤ a m.
An exact proof term for the current goal is La2 m Lm n H2.
We will prove a m ≤ b m.
Apply H1 m Hm to the current goal.
Assume H _.
Apply H to the current goal.
Assume H _.
An exact proof term for the current goal is H.
Assume H2: n = m.
rewrite the current goal using H2 (from right to left).
We will prove a n ≤ b n.
An exact proof term for the current goal is Labn.
Assume H2: m ∈ n.
We will prove a n ≤ b m.
Apply SNoLe_tra (a n) (b n) (b m) (La1 n Hn) (Lb1 n Hn) (Lb1 m Hm) to the current goal.
We will prove a n ≤ b n.
An exact proof term for the current goal is Labn.
We will prove b n ≤ b m.
An exact proof term for the current goal is Lb2 n Ln m H2.
Set L to be the term {q ∈ SNoS_ ω|∃n ∈ ω, q < a n}.
Set R to be the term {q ∈ SNoS_ ω|∃n ∈ ω, b n < q}.
Set x to be the term SNoCut L R.
We prove the intermediate claim LL: L ⊆ SNoS_ ω.
An exact proof term for the current goal is Sep_Subq (SNoS_ ω) (λq ⇒ ∃n ∈ ω, q < a n).
We prove the intermediate claim LR: R ⊆ SNoS_ ω.
An exact proof term for the current goal is Sep_Subq (SNoS_ ω) (λq ⇒ ∃n ∈ ω, b n < q).
We prove the intermediate claim LLR: SNoCutP L R.
We will prove (∀w ∈ L, SNo w) ∧ (∀y ∈ R, SNo y) ∧ (∀w ∈ L, ∀y ∈ R, w < y).
Apply and3I to the current goal.
Let w be given.
Assume Hw: w ∈ L.
Apply SepE (SNoS_ ω) (λq ⇒ ∃m ∈ ω, q < a m) w Hw to the current goal.
Assume H2: w ∈ SNoS_ ω.
Assume H3.
Apply H3 to the current goal.
Let n be given.
Assume H3.
Apply H3 to the current goal.
Assume Hn: n ∈ ω.
Assume H3: w < a n.
Apply SNoS_E2 ω omega_ordinal w H2 to the current goal.
Assume Hw1 Hw2 Hw3 Hw4.
An exact proof term for the current goal is Hw3.
Let z be given.
Assume Hz: z ∈ R.
Apply SepE (SNoS_ ω) (λq ⇒ ∃m ∈ ω, b m < q) z Hz to the current goal.
Assume H2: z ∈ SNoS_ ω.
Assume H3.
Apply H3 to the current goal.
Let m be given.
Assume H3.
Apply H3 to the current goal.
Assume Hm: m ∈ ω.
Assume H3: b m < z.
Apply SNoS_E2 ω omega_ordinal z H2 to the current goal.
Assume Hz1 Hz2 Hz3 Hz4.
An exact proof term for the current goal is Hz3.
Let w be given.
Assume Hw: w ∈ L.
Let z be given.
Assume Hz: z ∈ R.
Apply SepE (SNoS_ ω) (λq ⇒ ∃m ∈ ω, q < a m) w Hw to the current goal.
Assume H2: w ∈ SNoS_ ω.
Assume H3.
Apply H3 to the current goal.
Let n be given.
Assume H3.
Apply H3 to the current goal.
Assume Hn: n ∈ ω.
Assume H3: w < a n.
Apply SNoS_E2 ω omega_ordinal w H2 to the current goal.
Assume Hw1 Hw2 Hw3 Hw4.
Apply SepE (SNoS_ ω) (λq ⇒ ∃m ∈ ω, b m < q) z Hz to the current goal.
Assume H4: z ∈ SNoS_ ω.
Assume H5.
Apply H5 to the current goal.
Let m be given.
Assume H5.
Apply H5 to the current goal.
Assume Hm: m ∈ ω.
Assume H5: b m < z.
Apply SNoS_E2 ω omega_ordinal z H4 to the current goal.
Assume Hz1 Hz2 Hz3 Hz4.
We will prove w < z.
Apply SNoLt_tra w (a n) z Hw3 (La1 n Hn) Hz3 H3 to the current goal.
We will prove a n < z.
Apply SNoLeLt_tra (a n) (b m) z (La1 n Hn) (Lb1 m Hm) Hz3 to the current goal.
We will prove a n ≤ b m.
An exact proof term for the current goal is Lab n Hn m Hm.
We will prove b m < z.
An exact proof term for the current goal is H5.
Apply SNoCutP_SNoCut_impred L R LLR to the current goal.
Assume HLR1: SNo (SNoCut L R).
Assume HLR2: SNoLev (SNoCut L R) ∈ ordsucc ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Assume HLR3: ∀w ∈ L, w < SNoCut L R.
Assume HLR4: ∀y ∈ R, SNoCut L R < y.
Assume HLR5: ∀z, SNo z → (∀x ∈ L, x < z) → (∀y ∈ R, z < y) → SNoLev (SNoCut L R) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z.
We prove the intermediate claim Lax: ∀n ∈ ω, a n ≤ x.
Let n be given.
Assume Hn.
Apply SNo_approx_real_rep (a n) (ap_Pi ω (λ_ ⇒ real) a n Ha Hn) to the current goal.
Let f be given.
Assume Hf.
Let g be given.
Assume Hg Hf1 Hf2 Hf3 Hg1 Hg2 Hg3 Hfg Hanfg.
rewrite the current goal using Hanfg (from left to right).
We will prove SNoCut {f m|m ∈ ω} {g m|m ∈ ω} ≤ SNoCut L R.
Apply SNoCut_Le {f m|m ∈ ω} {g m|m ∈ ω} L R to the current goal.
We will prove SNoCutP {f m|m ∈ ω} {g m|m ∈ ω}.
An exact proof term for the current goal is Hfg.
We will prove SNoCutP L R.
An exact proof term for the current goal is LLR.
Let w be given.
Assume Hw: w ∈ {f m|m ∈ ω}.
We will prove w < x.
Apply ReplE_impred ω (λm ⇒ f m) w Hw to the current goal.
Let m be given.
Assume Hm: m ∈ ω.
Assume Hwm: w = f m.
rewrite the current goal using Hwm (from left to right).
We will prove f m < x.
Apply HLR3 to the current goal.
We will prove f m ∈ L.
Apply SepI to the current goal.
We will prove f m ∈ SNoS_ ω.
An exact proof term for the current goal is ap_Pi ω (λ_ ⇒ SNoS_ ω) f m Hf Hm.
We will prove ∃n ∈ ω, f m < a n.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn.
An exact proof term for the current goal is Hf1 m Hm.
Let z be given.
Assume Hz: z ∈ R.
rewrite the current goal using Hanfg (from right to left).
We will prove a n < z.
Apply SepE (SNoS_ ω) (λq ⇒ ∃m ∈ ω, b m < q) z Hz to the current goal.
Assume H2: z ∈ SNoS_ ω.
Assume H3.
Apply H3 to the current goal.
Let m be given.
Assume H3.
Apply H3 to the current goal.
Assume Hm: m ∈ ω.
Assume H3: b m < z.
Apply SNoS_E2 ω omega_ordinal z H2 to the current goal.
Assume Hz1 Hz2 Hz3 Hz4.
Apply SNoLeLt_tra (a n) (b m) z (La1 n Hn) (Lb1 m Hm) Hz3 to the current goal.
We will prove a n ≤ b m.
An exact proof term for the current goal is Lab n Hn m Hm.
An exact proof term for the current goal is H3.
We prove the intermediate claim Lxb: ∀n ∈ ω, x ≤ b n.
Let n be given.
Assume Hn.
We will prove x ≤ b n.
Apply SNo_approx_real_rep (b n) (ap_Pi ω (λ_ ⇒ real) b n Hb Hn) to the current goal.
Let f be given.
Assume Hf.
Let g be given.
Assume Hg Hf1 Hf2 Hf3 Hg1 Hg2 Hg3 Hfg Hbnfg.
rewrite the current goal using Hbnfg (from left to right).
We will prove SNoCut L R ≤ SNoCut {f m|m ∈ ω} {g m|m ∈ ω}.
Apply SNoCut_Le L R {f m|m ∈ ω} {g m|m ∈ ω} to the current goal.
We will prove SNoCutP L R.
An exact proof term for the current goal is LLR.
We will prove SNoCutP {f m|m ∈ ω} {g m|m ∈ ω}.
An exact proof term for the current goal is Hfg.
Let w be given.
Assume Hw: w ∈ L.
rewrite the current goal using Hbnfg (from right to left).
We will prove w < b n.
Apply SepE (SNoS_ ω) (λq ⇒ ∃m ∈ ω, q < a m) w Hw to the current goal.
Assume H2: w ∈ SNoS_ ω.
Assume H3.
Apply H3 to the current goal.
Let m be given.
Assume H3.
Apply H3 to the current goal.
Assume Hm: m ∈ ω.
Assume H3: w < a m.
Apply SNoS_E2 ω omega_ordinal w H2 to the current goal.
Assume Hw1 Hw2 Hw3 Hw4.
Apply SNoLtLe_tra w (a m) (b n) Hw3 (La1 m Hm) (Lb1 n Hn) to the current goal.
An exact proof term for the current goal is H3.
We will prove a m ≤ b n.
An exact proof term for the current goal is Lab m Hm n Hn.
Let z be given.
Assume Hz: z ∈ {g m|m ∈ ω}.
We will prove x < z.
Apply ReplE_impred ω (λm ⇒ g m) z Hz to the current goal.
Let m be given.
Assume Hm: m ∈ ω.
Assume Hzm: z = g m.
rewrite the current goal using Hzm (from left to right).
We will prove x < g m.
Apply HLR4 to the current goal.
We will prove g m ∈ R.
Apply SepI to the current goal.
We will prove g m ∈ SNoS_ ω.
An exact proof term for the current goal is ap_Pi ω (λ_ ⇒ SNoS_ ω) g m Hg Hm.
We will prove ∃n ∈ ω, b n < g m.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn.
An exact proof term for the current goal is Hg2 m Hm.
We prove the intermediate claim Laxb: ∀n ∈ ω, a n ≤ x ∧ x ≤ b n.
Let n be given.
Assume Hn.
Apply andI to the current goal.
An exact proof term for the current goal is Lax n Hn.
An exact proof term for the current goal is Lxb n Hn.
We prove the intermediate claim L1: ∀q ∈ SNoS_ ω, q ∈ L ∨ q ∈ R.
Let q be given.
Assume Hq.
Apply dneg to the current goal.
Assume HCq: ¬ (q ∈ L ∨ q ∈ R).
Apply SNoS_E2 ω omega_ordinal q Hq to the current goal.
Assume Hq1 Hq2 Hq3 Hq4.
We prove the intermediate claim L1a: ∀w ∈ L, w < q.
Let w be given.
Assume Hw: w ∈ L.
Apply SepE (SNoS_ ω) (λq ⇒ ∃m ∈ ω, q < a m) w Hw to the current goal.
Assume H2: w ∈ SNoS_ ω.
Assume H3.
Apply H3 to the current goal.
Let n be given.
Assume H3.
Apply H3 to the current goal.
Assume Hn: n ∈ ω.
Assume H3: w < a n.
Apply SNoS_E2 ω omega_ordinal w H2 to the current goal.
Assume Hw1 Hw2 Hw3 Hw4.
Apply SNoLtLe_or w q Hw3 Hq3 to the current goal.
Assume H4: w < q.
An exact proof term for the current goal is H4.
Assume H4: q ≤ w.
We will prove False.
Apply HCq to the current goal.
Apply orIL to the current goal.
We will prove q ∈ L.
Apply SepI to the current goal.
An exact proof term for the current goal is Hq.
We will prove ∃n ∈ ω, q < a n.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn.
We will prove q < a n.
An exact proof term for the current goal is SNoLeLt_tra q w (a n) Hq3 Hw3 (La1 n Hn) H4 H3.
We prove the intermediate claim L1b: ∀z ∈ R, q < z.
Let z be given.
Assume Hz: z ∈ R.
Apply SepE (SNoS_ ω) (λq ⇒ ∃m ∈ ω, b m < q) z Hz to the current goal.
Assume H2: z ∈ SNoS_ ω.
Assume H3.
Apply H3 to the current goal.
Let n be given.
Assume H3.
Apply H3 to the current goal.
Assume Hn: n ∈ ω.
Assume H3: b n < z.
Apply SNoS_E2 ω omega_ordinal z H2 to the current goal.
Assume Hz1 Hz2 Hz3 Hz4.
Apply SNoLtLe_or q z Hq3 Hz3 to the current goal.
Assume H4: q < z.
An exact proof term for the current goal is H4.
Assume H4: z ≤ q.
We will prove False.
Apply HCq to the current goal.
Apply orIR to the current goal.
We will prove q ∈ R.
Apply SepI to the current goal.
An exact proof term for the current goal is Hq.
We will prove ∃n ∈ ω, b n < q.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn.
We will prove b n < q.
An exact proof term for the current goal is SNoLtLe_tra (b n) z q (Lb1 n Hn) Hz3 Hq3 H3 H4.
Apply HLR5 q Hq3 L1a L1b to the current goal.
Assume H2: SNoLev x ⊆ SNoLev q.
Assume _.
Apply HC to the current goal.
We use x to witness the existential quantifier.
Apply andI to the current goal.
Apply SNoS_omega_real to the current goal.
We will prove x ∈ SNoS_ ω.
Apply SNoS_I ω omega_ordinal x (SNoLev x) to the current goal.
We will prove SNoLev x ∈ ω.
Apply omega_TransSet (ordsucc (SNoLev q)) (omega_ordsucc (SNoLev q) Hq1) to the current goal.
We will prove SNoLev x ∈ ordsucc (SNoLev q).
Apply ordinal_In_Or_Subq (SNoLev x) (ordsucc (SNoLev q)) (SNoLev_ordinal x HLR1) (ordinal_ordsucc (SNoLev q) Hq2) to the current goal.
Assume H3.
An exact proof term for the current goal is H3.
Assume H3: ordsucc (SNoLev q) ⊆ SNoLev x.
We will prove False.
Apply In_irref (SNoLev q) to the current goal.
Apply H2 to the current goal.
Apply H3 to the current goal.
Apply ordsuccI2 to the current goal.
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is HLR1.
An exact proof term for the current goal is Laxb.
Apply HC to the current goal.
We use x to witness the existential quantifier.
Apply andI to the current goal.
We will prove x ∈ real.
Apply real_I to the current goal.
We will prove x ∈ SNoS_ (ordsucc ω).
Apply SNoS_I (ordsucc ω) ordsucc_omega_ordinal x (SNoLev x) to the current goal.
We will prove SNoLev x ∈ ordsucc ω.
An exact proof term for the current goal is SNoCutP_SNoCut_omega L LL R LR LLR.
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is HLR1.
We will prove x ≠ ω.
Assume H2: x = ω.
We prove the intermediate claim Lbd1: x ≤ b 0.
An exact proof term for the current goal is Lxb 0 (nat_p_omega 0 nat_0).
Apply real_E (b 0) (ap_Pi ω (λ_ ⇒ real) b 0 Hb (nat_p_omega 0 nat_0)) to the current goal.
Assume Hb0a: SNo (b 0).
Assume _ _ _.
Assume Hb0b: b 0 < ω.
Assume _ _.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
Apply SNoLeLt_tra x (b 0) x HLR1 Hb0a HLR1 Lbd1 to the current goal.
We will prove b 0 < x.
rewrite the current goal using H2 (from left to right).
We will prove b 0 < ω.
An exact proof term for the current goal is Hb0b.
We will prove x ≠ - ω.
Assume H2: x = - ω.
We prove the intermediate claim Lbd2: a 0 ≤ x.
An exact proof term for the current goal is Lax 0 (nat_p_omega 0 nat_0).
Apply real_E (a 0) (ap_Pi ω (λ_ ⇒ real) a 0 Ha (nat_p_omega 0 nat_0)) to the current goal.
Assume Ha0a: SNo (a 0).
Assume _ _.
Assume Ha0b: - ω < a 0.
Assume _ _ _.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
Apply SNoLtLe_tra x (a 0) x HLR1 Ha0a HLR1 to the current goal.
We will prove x < a 0.
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is Ha0b.
We will prove a 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: q ∈ SNoS_ ω.
Assume Hq2: ∀k ∈ ω, abs_SNo (q + - x) < eps_ k.
We will prove False.
Apply SNoS_E2 ω omega_ordinal q Hq1 to the current goal.
Assume Hq1a Hq1b Hq1c Hq1d.
Apply L1 q Hq1 to the current goal.
Assume H2: q ∈ L.
Apply SepE (SNoS_ ω) (λq ⇒ ∃m ∈ ω, q < a m) q H2 to the current goal.
Assume _ H3.
Apply H3 to the current goal.
Let n be given.
Assume H3.
Apply H3 to the current goal.
Assume Hn: n ∈ ω.
Assume H3: q < a n.
Apply real_E (a n) (ap_Pi ω (λ_ ⇒ real) a n Ha Hn) to the current goal.
Assume _ _ _ _ _.
Assume H4: ∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - a n) < eps_ k) → q = a n.
Assume _.
We prove the intermediate claim L2: q = a n.
Apply H4 q Hq1 to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
We will prove abs_SNo (q + - a n) < eps_ k.
We prove the intermediate claim L2a: 0 < a n + - q.
An exact proof term for the current goal is SNoLt_minus_pos q (a n) Hq1c (La1 n Hn) H3.
We prove the intermediate claim L2b: a n ≤ x.
An exact proof term for the current goal is Lax n Hn.
We prove the intermediate claim L2c: 0 < x + - q.
Apply SNoLt_minus_pos q x Hq1c HLR1 to the current goal.
We will prove q < x.
An exact proof term for the current goal is SNoLtLe_tra q (a n) x Hq1c (La1 n Hn) HLR1 H3 L2b.
rewrite the current goal using abs_SNo_dist_swap q (a n) Hq1c (La1 n Hn) (from left to right).
We will prove abs_SNo (a n + - q) < eps_ k.
rewrite the current goal using pos_abs_SNo (a n + - q) L2a (from left to right).
We will prove a n + - q < eps_ k.
Apply SNoLeLt_tra (a n + - q) (x + - q) (eps_ k) (SNo_add_SNo (a n) (- q) (La1 n Hn) (SNo_minus_SNo q Hq1c)) (SNo_add_SNo x (- q) HLR1 (SNo_minus_SNo q Hq1c)) (SNo_eps_ k Hk) to the current goal.
We will prove a n + - q ≤ x + - q.
Apply add_SNo_Le1 (a n) (- q) x (La1 n Hn) (SNo_minus_SNo q Hq1c) HLR1 to the current goal.
We will prove a n ≤ x.
An exact proof term for the current goal is L2b.
We will prove x + - q < eps_ k.
rewrite the current goal using pos_abs_SNo (x + - q) L2c (from right to left).
rewrite the current goal using abs_SNo_dist_swap x q HLR1 Hq1c (from left to right).
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 L2 (from left to right) at position 2.
An exact proof term for the current goal is H3.
Assume H2: q ∈ R.
Apply SepE (SNoS_ ω) (λq ⇒ ∃m ∈ ω, b m < q) q H2 to the current goal.
Assume _ H3.
Apply H3 to the current goal.
Let n be given.
Assume H3.
Apply H3 to the current goal.
Assume Hn: n ∈ ω.
Assume H3: b n < q.
Apply real_E (b n) (ap_Pi ω (λ_ ⇒ real) b n Hb Hn) to the current goal.
Assume _ _ _ _ _.
Assume H4: ∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - b n) < eps_ k) → q = b n.
Assume _.
We prove the intermediate claim L3: q = b n.
Apply H4 q Hq1 to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
We will prove abs_SNo (q + - b n) < eps_ k.
We prove the intermediate claim L3a: 0 < q + - b n.
An exact proof term for the current goal is SNoLt_minus_pos (b n) q (Lb1 n Hn) Hq1c H3.
We prove the intermediate claim L3b: x ≤ b n.
An exact proof term for the current goal is Lxb n Hn.
We prove the intermediate claim L3c: 0 < q + - x.
Apply SNoLt_minus_pos x q HLR1 Hq1c to the current goal.
We will prove x < q.
An exact proof term for the current goal is SNoLeLt_tra x (b n) q HLR1 (Lb1 n Hn) Hq1c L3b H3.
We will prove abs_SNo (q + - b n) < eps_ k.
rewrite the current goal using pos_abs_SNo (q + - b n) L3a (from left to right).
We will prove q + - b n < eps_ k.
Apply SNoLeLt_tra (q + - b n) (q + - x) (eps_ k) (SNo_add_SNo q (- b n) Hq1c (SNo_minus_SNo (b n) (Lb1 n Hn))) (SNo_add_SNo q (- x) Hq1c (SNo_minus_SNo x HLR1)) (SNo_eps_ k Hk) to the current goal.
We will prove q + - b n ≤ q + - x.
Apply add_SNo_Le2 q (- b n) (- x) Hq1c (SNo_minus_SNo (b n) (Lb1 n Hn)) (SNo_minus_SNo x HLR1) to the current goal.
We will prove - b n ≤ - x.
An exact proof term for the current goal is minus_SNo_Le_contra x (b n) HLR1 (Lb1 n Hn) L3b.
We will prove q + - x < eps_ k.
rewrite the current goal using pos_abs_SNo (q + - x) L3c (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 L3 (from left to right) at position 1.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is Laxb.
∎