Let x be given.
Assume Hx1 Hx2 Hx3.
Apply SNoS_E2 (ordsucc ω) ordsucc_omega_ordinal x Hx1 to the current goal.
Assume Hx1a Hx1b Hx1c Hx1d.
Apply SNoS_ordsucc_omega_bdd_above x Hx1 Hx3 to the current goal.
Let N be given.
Assume HN.
Apply HN to the current goal.
Assume HN1: N ∈ ω.
Assume HN2: x < N.
We prove the intermediate claim LN: SNo N.
An exact proof term for the current goal is omega_SNo N HN1.
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN1.
We will prove eps_ N * x < 1.
Apply SNoLt_tra (eps_ N * x) (eps_ N * N) 1 (SNo_mul_SNo (eps_ N) x (SNo_eps_ N HN1) Hx1c) (SNo_mul_SNo (eps_ N) N (SNo_eps_ N HN1) LN) SNo_1 to the current goal.
We will prove eps_ N * x < eps_ N * N.
Apply pos_mul_SNo_Lt (eps_ N) x N (SNo_eps_ N HN1) (SNo_eps_pos N HN1) Hx1c LN to the current goal.
We will prove x < N.
An exact proof term for the current goal is HN2.
We will prove eps_ N * N < 1.
Apply SNoLtLe_or (eps_ N * N) 1 (SNo_mul_SNo (eps_ N) N (SNo_eps_ N HN1) LN) SNo_1 to the current goal.
Assume H1: eps_ N * N < 1.
An exact proof term for the current goal is H1.
Assume H1: 1 ≤ eps_ N * N.
We will prove False.
We prove the intermediate claim L2N: SNo (2 ^ N).
An exact proof term for the current goal is SNo_exp_SNo_nat 2 SNo_2 N (omega_nat_p N HN1).
We prove the intermediate claim L1: 2 ^ N ≤ 2 ^ N * eps_ N * N.
rewrite the current goal using mul_SNo_oneR (2 ^ N) L2N (from right to left) at position 1.
We will prove 2 ^ N * 1 ≤ 2 ^ N * eps_ N * N.
Apply nonneg_mul_SNo_Le (2 ^ N) 1 (eps_ N * N) L2N to the current goal.
We will prove 0 ≤ 2 ^ N.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is exp_SNo_nat_pos 2 SNo_2 SNoLt_0_2 N (omega_nat_p N HN1).
An exact proof term for the current goal is SNo_1.
An exact proof term for the current goal is SNo_mul_SNo (eps_ N) N (SNo_eps_ N HN1) LN.
We will prove 1 ≤ eps_ N * N.
An exact proof term for the current goal is H1.
Apply SNoLt_irref (2 ^ N) to the current goal.
We will prove 2 ^ N < 2 ^ N.
Apply SNoLeLt_tra (2 ^ N) N (2 ^ N) L2N LN L2N to the current goal.
We will prove 2 ^ N ≤ N.
rewrite the current goal using mul_SNo_oneL N LN (from right to left) at position 2.
We will prove 2 ^ N ≤ 1 * N.
rewrite the current goal using mul_SNo_eps_power_2' N (omega_nat_p N HN1) (from right to left) at position 2.
We will prove 2 ^ N ≤ (2 ^ N * eps_ N) * N.
rewrite the current goal using mul_SNo_assoc (2 ^ N) (eps_ N) N L2N (SNo_eps_ N HN1) LN (from right to left).
An exact proof term for the current goal is L1.
We will prove N < 2 ^ N.
An exact proof term for the current goal is exp_SNo_2_bd N (omega_nat_p N HN1).
∎