induction u with
| zero => simp
| succ u h =>
  rw [Nat.add_succ, Nat.pow_succ, Nat.mul_two]
  rw [← Nat.add_one]
  apply Nat.add_lt_add h
  apply Nat.one_lt_pow <;> linarith
case intro
u : ℕ
⊢ Nat.succ (2 + u) < 2 ^ (2 + u)
no goals