simp [Nat.succ_eq_add_one] at *
case H3
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (Nat.succ n) = 2 ^ Nat.succ n + 3 ^ Nat.succ n
⊢ a (Nat.succ (Nat.succ n)) = 2 ^ Nat.succ (Nat.succ n) + 3 ^ Nat.succ (Nat.succ n)
case H3
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (n + 1) = 2 ^ (n + 1) + 3 ^ (n + 1)
⊢ a (n + 1 + 1) = 2 ^ (n + 1 + 1) + 3 ^ (n + 1 + 1)