Let n be given.

Assume Hn.

Use transitivity with and eps_ n * 2 ^ n.

Apply mul_SNo_com to the current goal.

An exact proof term for the current goal is SNo_exp_SNo_nat 2 SNo_2 n Hn.

An exact proof term for the current goal is SNo_eps_ n (nat_p_omega n Hn).

An exact proof term for the current goal is mul_SNo_eps_power_2 n Hn.

∎