Let n be given.
Assume Hn.
We will prove eps_ n ≤ 1.
rewrite the current goal using mul_SNo_oneR (eps_ n) (SNo_eps_ n Hn) (from right to left).
We will prove eps_ n * 1 ≤ 1.
rewrite the current goal using mul_SNo_eps_power_2 n (omega_nat_p n Hn) (from right to left) at position 2.
We will prove eps_ n * 1 ≤ eps_ n * 2 ^ n.
Apply nonneg_mul_SNo_Le (eps_ n) 1 (2 ^ n) (SNo_eps_ n Hn) to the current goal.
We will prove 0 ≤ eps_ n.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNo_eps_pos n Hn.
An exact proof term for the current goal is SNo_1.
We will prove SNo (2 ^ n).
Apply SNo_exp_SNo_nat to the current goal.
An exact proof term for the current goal is SNo_2.
We will prove nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn.
We will prove 1 ≤ 2 ^ n.
Apply exp_SNo_1_bd 2 SNo_2 to the current goal.
We will prove 1 ≤ 2.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNoLt_1_2.
We will prove nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn.
∎