Let x be given.
Assume Hx: x ∈ SNoS_ ω.
Apply SNoS_E2 ω omega_ordinal x Hx to the current goal.
Assume Hx1 Hx2 Hx3 Hx4.
Apply real_I to the current goal.
We will prove x ∈ SNoS_ (ordsucc ω).
Apply SNoS_Subq ω (ordsucc ω) omega_ordinal ordsucc_omega_ordinal (ordsuccI1 ω) to the current goal.
An exact proof term for the current goal is Hx.
We will prove x ≠ ω.
Assume H1: x = ω.
Apply In_irref (SNoLev x) to the current goal.
We will prove SNoLev x ∈ SNoLev x.
rewrite the current goal using H1 (from left to right) at position 2.
We will prove SNoLev x ∈ SNoLev ω.
rewrite the current goal using ordinal_SNoLev ω omega_ordinal (from left to right).
An exact proof term for the current goal is Hx1.
We will prove x ≠ - ω.
Assume H1: x = - ω.
Apply In_irref (SNoLev x) to the current goal.
We will prove SNoLev x ∈ SNoLev x.
rewrite the current goal using H1 (from left to right) at position 2.
We will prove SNoLev x ∈ SNoLev (- ω).
rewrite the current goal using minus_SNo_Lev ω SNo_omega (from left to right).
We will prove SNoLev x ∈ SNoLev ω.
rewrite the current goal using ordinal_SNoLev ω omega_ordinal (from left to right).
An exact proof term for the current goal is Hx1.
Let q be given.
Assume Hq: q ∈ SNoS_ ω.
Assume H1: ∀k ∈ ω, abs_SNo (q + - x) < eps_ k.
Apply SNoS_E2 ω omega_ordinal q Hq to the current goal.
Assume Hq1 Hq2 Hq3 Hq4.
We will prove q = x.
Apply SNoLt_trichotomy_or_impred q x Hq3 Hx3 to the current goal.
Assume Hqx: q < x.
We will prove False.
We prove the intermediate claim L1: 0 < x + - q.
Apply SNoLt_minus_pos q x Hq3 Hx3 to the current goal.
An exact proof term for the current goal is Hqx.
We prove the intermediate claim L2: x + - q ∈ SNoS_ ω.
An exact proof term for the current goal is add_SNo_SNoS_omega x Hx (- q) (minus_SNo_SNoS_omega q Hq).
Apply SNoS_E2 ω omega_ordinal (x + - q) L2 to the current goal.
Assume H2: SNoLev (x + - q) ∈ ω.
Assume H3: ordinal (SNoLev (x + - q)).
Assume H4: SNo (x + - q).
Assume H5: SNo_ (SNoLev (x + - q)) (x + - q).
Apply SNoLt_irref (x + - q) to the current goal.
Apply SNoLt_tra (x + - q) (eps_ (SNoLev (x + - q))) (x + - q) H4 (SNo_eps_ (SNoLev (x + - q)) H2) H4 to the current goal.
We will prove x + - q < eps_ (SNoLev (x + - q)).
We prove the intermediate claim L3: abs_SNo (q + - x) = x + - q.
rewrite the current goal using abs_SNo_dist_swap q x Hq3 Hx3 (from left to right).
An exact proof term for the current goal is pos_abs_SNo (x + - q) L1.
rewrite the current goal using L3 (from right to left) at position 1.
An exact proof term for the current goal is H1 (SNoLev (x + - q)) H2.
We will prove eps_ (SNoLev (x + - q)) < x + - q.
Apply SNo_pos_eps_Lt (SNoLev (x + - q)) (omega_nat_p (SNoLev (x + - q)) H2) (x + - q) to the current goal.
We will prove (x + - q) ∈ SNoS_ (ordsucc (SNoLev (x + - q))).
Apply SNoS_I (ordsucc (SNoLev (x + - q))) (ordinal_ordsucc (SNoLev (x + - q)) H3) (x + - q) (SNoLev (x + - q)) to the current goal.
Apply ordsuccI2 to the current goal.
An exact proof term for the current goal is H5.
An exact proof term for the current goal is L1.
Assume Hqx: q = x.
An exact proof term for the current goal is Hqx.
Assume Hxq: x < q.
We will prove False.
We prove the intermediate claim L4: 0 < q + - x.
Apply SNoLt_minus_pos x q Hx3 Hq3 to the current goal.
An exact proof term for the current goal is Hxq.
We prove the intermediate claim L5: q + - x ∈ SNoS_ ω.
An exact proof term for the current goal is add_SNo_SNoS_omega q Hq (- x) (minus_SNo_SNoS_omega x Hx).
Apply SNoS_E2 ω omega_ordinal (q + - x) L5 to the current goal.
Assume H2: SNoLev (q + - x) ∈ ω.
Assume H3: ordinal (SNoLev (q + - x)).
Assume H4: SNo (q + - x).
Assume H5: SNo_ (SNoLev (q + - x)) (q + - x).
Apply SNoLt_irref (q + - x) to the current goal.
Apply SNoLt_tra (q + - x) (eps_ (SNoLev (q + - x))) (q + - x) H4 (SNo_eps_ (SNoLev (q + - x)) H2) H4 to the current goal.
We will prove q + - x < eps_ (SNoLev (q + - x)).
We prove the intermediate claim L6: abs_SNo (q + - x) = q + - x.
An exact proof term for the current goal is pos_abs_SNo (q + - x) L4.
rewrite the current goal using L6 (from right to left) at position 1.
An exact proof term for the current goal is H1 (SNoLev (q + - x)) H2.
We will prove eps_ (SNoLev (q + - x)) < q + - x.
Apply SNo_pos_eps_Lt (SNoLev (q + - x)) (omega_nat_p (SNoLev (q + - x)) H2) (q + - x) to the current goal.
We will prove (q + - x) ∈ SNoS_ (ordsucc (SNoLev (q + - x))).
Apply SNoS_I (ordsucc (SNoLev (q + - x))) (ordinal_ordsucc (SNoLev (q + - x)) H3) (q + - x) (SNoLev (q + - x)) to the current goal.
Apply ordsuccI2 to the current goal.
An exact proof term for the current goal is H5.
An exact proof term for the current goal is L4.
∎