Let x be given.
Assume Hx H1.
Let k be given.
Assume Hk.
Apply H1 k Hk to the current goal.
Let q be given.
Assume Hq.
Apply Hq to the current goal.
Assume Hq1: q ∈ SNoS_ ω.
Assume Hq.
Apply Hq 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.
We prove the intermediate claim Lqk: SNo (q + eps_ k).
An exact proof term for the current goal is SNo_add_SNo q (eps_ k) Hq1c (SNo_eps_ k Hk).
We use (- (q + eps_ k)) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is minus_SNo_SNoS_omega (q + eps_ k) (add_SNo_SNoS_omega q Hq1 (eps_ k) (SNo_eps_SNoS_omega k Hk)).
Apply andI to the current goal.
We will prove - (q + eps_ k) < - x.
Apply minus_SNo_Lt_contra x (q + eps_ k) Hx Lqk to the current goal.
We will prove x < q + eps_ k.
An exact proof term for the current goal is Hq3.
We will prove - x < - (q + eps_ k) + eps_ k.
rewrite the current goal using minus_add_SNo_distr q (eps_ k) Hq1c (SNo_eps_ k Hk) (from left to right).
We will prove - x < (- q + - eps_ k) + eps_ k.
rewrite the current goal using add_SNo_minus_R2' (- q) (eps_ k) (SNo_minus_SNo q Hq1c) (SNo_eps_ k Hk) (from left to right).
We will prove - x < - q.
Apply minus_SNo_Lt_contra q x Hq1c Hx to the current goal.
We will prove q < x.
An exact proof term for the current goal is Hq2.
∎