Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
Assume Hxpos Hynneg.
Apply real_E x Hx to the current goal.
Assume Hx1 Hx2 Hx3 Hx4 Hx5.
Assume Hx6: ∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x.
Assume Hx7.
We prove the intermediate claim L1: ∃n ∈ ω, eps_ n ≤ x.
Apply dneg to the current goal.
Assume HC: ¬ (∃n ∈ ω, eps_ n ≤ x).
We prove the intermediate claim L1a: 0 = x.
Apply Hx6 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 Hx1) (from left to right).
We will prove abs_SNo (- x) < eps_ k.
rewrite the current goal using abs_SNo_minus x Hx1 (from left to right).
We will prove abs_SNo x < eps_ k.
rewrite the current goal using pos_abs_SNo x Hxpos (from left to right).
We will prove x < eps_ k.
Apply SNoLtLe_or x (eps_ k) Hx1 (SNo_eps_ k Hk) to the current goal.
Assume H1.
An exact proof term for the current goal is H1.
Assume H1: eps_ k ≤ x.
We will prove False.
Apply HC to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk.
An exact proof term for the current goal is H1.
Apply SNoLt_irref x to the current goal.
rewrite the current goal using L1a (from right to left) at position 1.
An exact proof term for the current goal is Hxpos.
Apply L1 to the current goal.
Let n be given.
Assume Hn.
Apply Hn to the current goal.
Assume Hn1: n ∈ ω.
Assume Hn2: eps_ n ≤ x.
We prove the intermediate claim L2n: nat_p (2 ^ n).
Apply nat_exp_SNo_nat to the current goal.
An exact proof term for the current goal is nat_2.
An exact proof term for the current goal is omega_nat_p n Hn1.
We prove the intermediate claim L2nb: 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 L2nc: 0 ≤ 2 ^ n.
Apply ordinal_SNoLev_max_2 to the current goal.
We will prove ordinal (2 ^ n).
Apply nat_p_ordinal to the current goal.
An exact proof term for the current goal is L2n.
An exact proof term for the current goal is SNo_0.
We will prove SNoLev 0 ∈ ordsucc (2 ^ n).
rewrite the current goal using SNoLev_0 (from left to right).
We will prove 0 ∈ ordsucc (2 ^ n).
Apply nat_0_in_ordsucc to the current goal.
An exact proof term for the current goal is L2n.
We prove the intermediate claim L2: 1 ≤ 2 ^ n * x.
rewrite the current goal using mul_SNo_eps_power_2' n (omega_nat_p n Hn1) (from right to left) at position 1.
We will prove 2 ^ n * eps_ n ≤ 2 ^ n * x.
Apply nonneg_mul_SNo_Le (2 ^ n) (eps_ n) x L2nb L2nc (SNo_eps_ n Hn1) Hx1 to the current goal.
We will prove eps_ n ≤ x.
An exact proof term for the current goal is Hn2.
Apply real_E y Hy to the current goal.
Assume Hy1 Hy2.
Assume Hy3: y ∈ SNoS_ (ordsucc ω).
Assume Hy4.
Assume Hy5: y < ω.
Assume Hy6 Hy7.
Apply SNoS_ordsucc_omega_bdd_above y Hy3 Hy5 to the current goal.
Let N be given.
Assume HN.
Apply HN to the current goal.
Assume HN1: N ∈ ω.
Assume HN2: y < N.
We use (N * 2 ^ n) to witness the existential quantifier.
Apply andI to the current goal.
We will prove N * 2 ^ n ∈ ω.
We will prove N * 2 ^ n ∈ ω.
rewrite the current goal using mul_nat_mul_SNo N HN1 (2 ^ n) (nat_p_omega (2 ^ n) L2n) (from right to left).
We will prove mul_nat N (2 ^ n) ∈ ω.
Apply nat_p_omega to the current goal.
Apply mul_nat_p to the current goal.
An exact proof term for the current goal is omega_nat_p N HN1.
An exact proof term for the current goal is L2n.
We will prove y ≤ (N * 2 ^ n) * x.
We prove the intermediate claim LN1: SNo N.
An exact proof term for the current goal is omega_SNo N HN1.
We prove the intermediate claim LN2n: SNo (N * 2 ^ n).
Apply SNo_mul_SNo to the current goal.
An exact proof term for the current goal is LN1.
An exact proof term for the current goal is L2nb.
Apply SNoLe_tra y N ((N * 2 ^ n) * x) Hy1 LN1 (SNo_mul_SNo (N * 2 ^ n) x LN2n Hx1) to the current goal.
We will prove y ≤ N.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is HN2.
We will prove N ≤ (N * 2 ^ n) * x.
rewrite the current goal using mul_SNo_oneR N LN1 (from right to left) at position 1.
We will prove N * 1 ≤ (N * 2 ^ n) * x.
rewrite the current goal using mul_SNo_assoc N (2 ^ n) x LN1 L2nb Hx1 (from right to left).
We will prove N * 1 ≤ N * (2 ^ n * x).
We prove the intermediate claim LN2: 0 ≤ N.
Apply ordinal_SNoLev_max_2 to the current goal.
We will prove ordinal N.
Apply nat_p_ordinal to the current goal.
An exact proof term for the current goal is omega_nat_p N HN1.
An exact proof term for the current goal is SNo_0.
We will prove SNoLev 0 ∈ ordsucc N.
rewrite the current goal using SNoLev_0 (from left to right).
We will prove 0 ∈ ordsucc N.
Apply nat_0_in_ordsucc to the current goal.
An exact proof term for the current goal is omega_nat_p N HN1.
Apply nonneg_mul_SNo_Le N 1 (2 ^ n * x) LN1 LN2 SNo_1 to the current goal.
We will prove SNo (2 ^ n * x).
An exact proof term for the current goal is SNo_mul_SNo (2 ^ n) x L2nb Hx1.
We will prove 1 ≤ 2 ^ n * x.
An exact proof term for the current goal is L2.
∎