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 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.
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 Hp H1c H1a H1 L2 L1 H4 L3.
∎