cases h2 with | intro u hu =>
rw [hu]
clear a hu
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
a : ℕ
h2 : ∃ k, a = 2 + k
⊢ Nat.succ a < 2 ^ a
no goals