calc
  a (n + 2) 
    = (5 : ℤ) * (2 ^ (n + 1) + 3 ^ (n + 1)) - 
        6 * (2 ^ n + 3 ^ n) := by linarith [helper n]
  _ = (2 : ℤ) ^ (n + 2) + 3 ^ (n + 2) := by ring
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)
no goals