Let x be given.
Assume HxR Hxnn.
Apply real_E x HxR to the current goal.
Assume Hx1: SNo x.
Assume Hx2: SNoLev x ∈ ordsucc ω.
Assume Hx3: x ∈ SNoS_ (ordsucc ω).
Assume Hx4: - ω < x.
Assume Hx5: x < ω.
Assume Hx6: ∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x.
Assume Hx7: ∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k.
We prove the intermediate claim L1: ∀m, nat_p m → x < m → ∃n ∈ ω, n ≤ x ∧ x < ordsucc n.
Apply nat_ind to the current goal.
Assume H1: x < 0.
We will prove False.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
An exact proof term for the current goal is SNoLeLt_tra 0 x 0 SNo_0 Hx1 SNo_0 Hxnn H1.
Let m be given.
Assume Hm.
Assume IHm: x < m → ∃n ∈ ω, n ≤ x ∧ x < ordsucc n.
Assume H2: x < ordsucc m.
Apply SNoLtLe_or x m Hx1 (nat_p_SNo m Hm) to the current goal.
Assume H3: x < m.
Apply IHm to the current goal.
We will prove x < m.
An exact proof term for the current goal is H3.
Assume H3: m ≤ x.
We use m to witness the existential quantifier.
Apply andI to the current goal.
We will prove m ∈ ω.
An exact proof term for the current goal is nat_p_omega m Hm.
Apply andI to the current goal.
We will prove m ≤ x.
An exact proof term for the current goal is H3.
We will prove x < ordsucc m.
An exact proof term for the current goal is H2.
Apply Hx7 0 (nat_p_omega 0 nat_0) to the current goal.
Let q be given.
Assume H.
Apply H to the current goal.
Assume Hq: q ∈ SNoS_ ω.
Assume H.
Apply H to the current goal.
Assume Hqx: q < x.
rewrite the current goal using eps_0_1 (from left to right).
Assume Hxq1: x < q + 1.
Apply SNoS_E ω omega_ordinal q Hq to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ ω.
Assume H1: SNo_ m q.
We prove the intermediate claim Lq: SNo q.
An exact proof term for the current goal is SNo_SNo m (nat_p_ordinal m (omega_nat_p m Hm)) q H1.
Apply L1 (ordsucc m) to the current goal.
We will prove nat_p (ordsucc m).
Apply nat_ordsucc to the current goal.
Apply omega_nat_p to the current goal.
An exact proof term for the current goal is Hm.
We will prove x < ordsucc m.
Apply SNoLtLe_tra x (q + 1) (ordsucc m) Hx1 (SNo_add_SNo q 1 Lq SNo_1) (nat_p_SNo (ordsucc m) (nat_ordsucc m (omega_nat_p m Hm))) Hxq1 to the current goal.
We will prove q + 1 ≤ ordsucc m.
We prove the intermediate claim Lq1: SNo (q + 1).
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Lq.
An exact proof term for the current goal is SNo_1.
Apply ordinal_SNoLev_max_2 (ordsucc m) (nat_p_ordinal (ordsucc m) (nat_ordsucc m (omega_nat_p m Hm))) (q + 1) to the current goal.
We will prove SNo (q + 1).
An exact proof term for the current goal is Lq1.
We will prove SNoLev (q + 1) ∈ ordsucc (ordsucc m).
Apply ordinal_In_Or_Subq (SNoLev (q + 1)) (ordsucc m) (SNoLev_ordinal (q + 1) Lq1) (nat_p_ordinal (ordsucc m) (nat_ordsucc m (omega_nat_p m Hm))) to the current goal.
Assume H2: SNoLev (q + 1) ∈ ordsucc m.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is H2.
Assume H2: ordsucc m ⊆ SNoLev (q + 1).
We prove the intermediate claim L2: SNoLev (q + 1) ⊆ ordsucc m.
Apply Subq_tra (SNoLev (q + 1)) (SNoLev q + SNoLev 1) to the current goal.
We will prove SNoLev (q + 1) ⊆ SNoLev q + SNoLev 1.
Apply add_SNo_Lev_bd to the current goal.
An exact proof term for the current goal is Lq.
An exact proof term for the current goal is SNo_1.
We will prove SNoLev q + SNoLev 1 ⊆ ordsucc m.
rewrite the current goal using SNoLev_uniq2 m (nat_p_ordinal m (omega_nat_p m Hm)) q H1 (from left to right).
rewrite the current goal using ordinal_SNoLev 1 (nat_p_ordinal 1 nat_1) (from left to right).
We will prove m + 1 ⊆ ordsucc m.
rewrite the current goal using add_SNo_1_ordsucc m Hm (from left to right).
Apply Subq_ref to the current goal.
We prove the intermediate claim L3: SNoLev (q + 1) = ordsucc m.
Apply set_ext to the current goal.
An exact proof term for the current goal is L2.
An exact proof term for the current goal is H2.
rewrite the current goal using L3 (from left to right).
Apply ordsuccI2 to the current goal.
∎