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 Hq.
Apply Hq to the current goal.
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).
Apply minus_SNo_Lt_contra q x Hq1c Hx to the current goal.
An exact proof term for the current goal is Hq2.