lean_workbook_plus_82788

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_82788 (a : ℕ → ℤ) (a0 : a 0 = 2) (a_rec : ∀ n, a (n + 1) + 3 * a n = n ^ 3 - 1) : ∃ f : ℕ → ℤ, ∀ n, a n = f n   :=  by sorry