rw [← Nat.add_one]
case intro.succ
u : ℕ
h : Nat.succ (2 + u) < 2 ^ (2 + u)
⊢ Nat.succ (Nat.succ (2 + u)) < 2 ^ (2 + u) + 2 ^ (2 + u)
case intro.succ
u : ℕ
h : Nat.succ (2 + u) < 2 ^ (2 + u)
⊢ 2 + u + 1 + 1 < 2 ^ (2 + u) + 2 ^ (2 + u)