Let n be given.

Assume Hn.

Assume IHn: n < 2 ^ n.

We prove the intermediate claim Ln: SNo n.

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

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 Hn.

We will prove ordsucc n < 2 ^ (ordsucc n).

rewrite the current goal using exp_SNo_nat_S 2 SNo_2 n Hn (from left to right).

We will prove ordsucc n < 2 * 2 ^ n.

rewrite the current goal using add_SNo_1_ordsucc n (nat_p_omega n Hn) (from right to left).

We will prove n + 1 < 2 * 2 ^ n.

rewrite the current goal using add_SNo_1_1_2 (from right to left) at position 1.

We will prove n + 1 < (1 + 1) * 2 ^ n.

rewrite the current goal using mul_SNo_distrR 1 1 (2 ^ n) SNo_1 SNo_1 L2n (from left to right).

We will prove n + 1 < 1 * 2 ^ n + 1 * 2 ^ n.

rewrite the current goal using mul_SNo_oneL (2 ^ n) L2n (from left to right).

We will prove n + 1 < 2 ^ n + 2 ^ n.

Apply SNoLtLe_tra (n + 1) (2 ^ n + 1) (2 ^ n + 2 ^ n) (SNo_add_SNo n 1 Ln SNo_1) (SNo_add_SNo (2 ^ n) 1 L2n SNo_1) (SNo_add_SNo (2 ^ n) (2 ^ n) L2n L2n) to the current goal.

We will prove n + 1 < 2 ^ n + 1.

An exact proof term for the current goal is add_SNo_Lt1 n 1 (2 ^ n) Ln SNo_1 L2n IHn.

We will prove 2 ^ n + 1 ≤ 2 ^ n + 2 ^ n.

Apply add_SNo_Le2 (2 ^ n) 1 (2 ^ n) L2n SNo_1 L2n to the current goal.

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.

An exact proof term for the current goal is Hn.