Let x be given.
Assume Hx.
Let p be given.
Assume Hp.
Apply SepE (SNoS_ (ordsucc ω)) (λx ⇒ x ≠ ω ∧ x ≠ - ω ∧ (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x)) x Hx to the current goal.
Assume H1 H2.
Apply H2 to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: x ≠ ω.
Assume H3: x ≠ - ω.
Assume H4.
Apply SNoS_E2 (ordsucc ω) ordsucc_omega_ordinal x H1 to the current goal.
Assume H1a H1b H1c H1d.
We prove the intermediate claim L1: x < ω.
We prove the intermediate claim L1a: x ≤ ω.
Apply ordinal_SNoLev_max_2 ω omega_ordinal x H1c to the current goal.
We will prove SNoLev x ∈ ordsucc ω.
An exact proof term for the current goal is H1a.
Apply SNoLeE x ω H1c SNo_omega L1a to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume H: x = ω.
We will prove False.
An exact proof term for the current goal is H2 H.
We prove the intermediate claim L2: - ω < x.
We prove the intermediate claim L2a: - ω ≤ x.
Apply mordinal_SNoLev_min_2 ω omega_ordinal x H1c to the current goal.
We will prove SNoLev x ∈ ordsucc ω.
An exact proof term for the current goal is H1a.
Apply SNoLeE (- ω) x (SNo_minus_SNo ω SNo_omega) H1c L2a to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume H: - ω = x.
We will prove False.
Apply H3 to the current goal.
Use symmetry.
An exact proof term for the current goal is H.
We prove the intermediate claim L3: ∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k.
An exact proof term for the current goal is SNoS_ordsucc_omega_bdd_drat_intvl x H1 L2 L1.
An exact proof term for the current goal is Hp H1c H1a H1 L2 L1 H4 L3.
∎