Let x be given.
Assume Hx.
Apply SNoS_E2 ω omega_ordinal x Hx to the current goal.
Assume Hx1 Hx2 Hx3 Hx4.
Let k be given.
Assume Hk.
We will prove ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k.
We prove the intermediate claim Lk1: SNo (eps_ (ordsucc k)).
An exact proof term for the current goal is SNo_eps_ (ordsucc k) (omega_ordsucc k Hk).
We use x + - eps_ (ordsucc k) to witness the existential quantifier.
Apply andI to the current goal.
We will prove x + - eps_ (ordsucc k) ∈ SNoS_ ω.
An exact proof term for the current goal is add_SNo_SNoS_omega x Hx (- eps_ (ordsucc k)) (minus_SNo_SNoS_omega (eps_ (ordsucc k)) (SNo_eps_SNoS_omega (ordsucc k) (omega_ordsucc k Hk))).
Apply andI to the current goal.
We will prove x + - eps_ (ordsucc k) < x.
Apply add_SNo_minus_Lt1b x (eps_ (ordsucc k)) x Hx3 Lk1 Hx3 to the current goal.
We will prove x < x + eps_ (ordsucc k).
An exact proof term for the current goal is add_SNo_eps_Lt x Hx3 (ordsucc k) (omega_ordsucc k Hk).
We will prove x < (x + - eps_ (ordsucc k)) + eps_ k.
rewrite the current goal using eps_ordsucc_half_add k (omega_nat_p k Hk) (from right to left).
We will prove x < (x + - eps_ (ordsucc k)) + (eps_ (ordsucc k) + eps_ (ordsucc k)).
rewrite the current goal using add_SNo_com_4_inner_mid x (- eps_ (ordsucc k)) (eps_ (ordsucc k)) (eps_ (ordsucc k)) Hx3 (SNo_minus_SNo (eps_ (ordsucc k)) Lk1) Lk1 Lk1 (from left to right).
We will prove x < (x + eps_ (ordsucc k)) + (- eps_ (ordsucc k) + eps_ (ordsucc k)).
rewrite the current goal using add_SNo_minus_SNo_linv (eps_ (ordsucc k)) Lk1 (from left to right).
rewrite the current goal using add_SNo_0R (x + eps_ (ordsucc k)) (SNo_add_SNo x (eps_ (ordsucc k)) Hx3 Lk1) (from left to right).
We will prove x < x + eps_ (ordsucc k).
An exact proof term for the current goal is add_SNo_eps_Lt x Hx3 (ordsucc k) (omega_ordsucc k Hk).
∎