Let x be given.
Assume Hx Hx0 Hx2 Hx3.
Let k be given.
Assume Hk.
Let p be given.
Assume Hp.
Apply Hx3 k Hk to the current goal.
Let q be given.
Assume H.
Apply H to the current goal.
Assume Hq1: q ∈ SNoS_ ω.
Assume H.
Apply H to the current goal.
Assume Hq2: q < x.
Assume Hq3: x < q + eps_ k.
Apply SNoS_E2 ω omega_ordinal q Hq1 to the current goal.
Assume Hq1a Hq1b Hq1c Hq1d.
Apply SNoLtLe_or 0 q SNo_0 Hq1c to the current goal.
Assume H1: 0 < q.
An exact proof term for the current goal is Hp q Hq1 H1 Hq2 Hq3.
Assume H1: q ≤ 0.
Apply xm (∀k' ∈ ω, x < eps_ k') to the current goal.
Assume H2: ∀k' ∈ ω, x < eps_ k'.
We will prove False.
We prove the intermediate claim L1: 0 = x.
Apply Hx2 0 (omega_SNoS_omega 0 (nat_p_omega 0 nat_0)) to the current goal.
Let k' be given.
Assume Hk': k' ∈ ω.
We will prove abs_SNo (0 + - x) < eps_ k'.
rewrite the current goal using add_SNo_0L (- x) (SNo_minus_SNo x Hx) (from left to right).
We will prove abs_SNo (- x) < eps_ k'.
rewrite the current goal using abs_SNo_minus x Hx (from left to right).
We will prove abs_SNo x < eps_ k'.
rewrite the current goal using pos_abs_SNo x Hx0 (from left to right).
An exact proof term for the current goal is H2 k' Hk'.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
rewrite the current goal using L1 (from right to left) at position 1.
An exact proof term for the current goal is Hx0.
Assume H2: ¬ (∀k' ∈ ω, x < eps_ k').
Apply dneg to the current goal.
Assume H3: ¬ p.
Apply H2 to the current goal.
Let k' be given.
Assume Hk': k' ∈ ω.
Apply SNoLtLe_or x (eps_ k') Hx (SNo_eps_ k' Hk') to the current goal.
Assume H4: x < eps_ k'.
An exact proof term for the current goal is H4.
Assume H4: eps_ k' ≤ x.
We prove the intermediate claim Lek': SNo (eps_ k').
Apply SNo_eps_ to the current goal.
An exact proof term for the current goal is Hk'.
We prove the intermediate claim LeSk': SNo (eps_ (ordsucc k')).
Apply SNo_eps_ to the current goal.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is Hk'.
We prove the intermediate claim LeSk'pos: 0 < eps_ (ordsucc k').
Apply SNo_eps_pos to the current goal.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is Hk'.
Apply H3 to the current goal.
Apply Hp (eps_ (ordsucc k')) to the current goal.
We will prove eps_ (ordsucc k') ∈ SNoS_ ω.
Apply SNo_eps_SNoS_omega to the current goal.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is Hk'.
We will prove 0 < eps_ (ordsucc k').
An exact proof term for the current goal is LeSk'pos.
We will prove eps_ (ordsucc k') < x.
Apply SNoLtLe_tra (eps_ (ordsucc k')) (eps_ k') x LeSk' Lek' Hx to the current goal.
We will prove eps_ (ordsucc k') < eps_ k'.
An exact proof term for the current goal is SNo_eps_decr (ordsucc k') (omega_ordsucc k' Hk') k' (ordsuccI2 k').
We will prove eps_ k' ≤ x.
An exact proof term for the current goal is H4.
We will prove x < eps_ (ordsucc k') + eps_ k.
We prove the intermediate claim L2: q < eps_ (ordsucc k').
Apply SNoLeLt_tra q 0 (eps_ (ordsucc k')) Hq1c SNo_0 LeSk' to the current goal.
We will prove q ≤ 0.
An exact proof term for the current goal is H1.
We will prove 0 < eps_ (ordsucc k').
An exact proof term for the current goal is LeSk'pos.
Apply SNoLt_tra x (q + eps_ k) (eps_ (ordsucc k') + eps_ k) Hx (SNo_add_SNo q (eps_ k) Hq1c (SNo_eps_ k Hk)) (SNo_add_SNo (eps_ (ordsucc k')) (eps_ k) LeSk' (SNo_eps_ k Hk)) to the current goal.
We will prove x < q + eps_ k.
An exact proof term for the current goal is Hq3.
We will prove q + eps_ k < eps_ (ordsucc k') + eps_ k.
Apply add_SNo_Lt1 q (eps_ k) (eps_ (ordsucc k')) Hq1c (SNo_eps_ k Hk) LeSk' to the current goal.
We will prove q < eps_ (ordsucc k').
An exact proof term for the current goal is L2.
∎