rw [Nat.add_succ, Nat.pow_succ, Nat.mul_two]
case intro.succ
u : ℕ
h : Nat.succ (2 + u) < 2 ^ (2 + u)
⊢ Nat.succ (2 + Nat.succ u) < 2 ^ (2 + Nat.succ u)
case intro.succ
u : ℕ
h : Nat.succ (2 + u) < 2 ^ (2 + u)
⊢ Nat.succ (Nat.succ (2 + u)) < 2 ^ (2 + u) + 2 ^ (2 + u)