Let m be given.
Assume Hm.
Let n be given.
Assume Hn.
We will prove (2 ^ m) * (2 * n + 1) ∈ ω.
Apply mul_SNo_In_omega to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_exp_SNo_nat 2 nat_2 m (omega_nat_p m Hm).
Apply add_SNo_In_omega to the current goal.
Apply mul_SNo_In_omega to the current goal.
An exact proof term for the current goal is nat_p_omega 2 nat_2.
An exact proof term for the current goal is Hn.
An exact proof term for the current goal is nat_p_omega 1 nat_1.
∎