lean_workbook_plus_69025

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_69025 (a : ℕ → ℤ) (a0 : a 0 = 0) (a1 : a 1 = -1) (a_rec : ∀ m, a (m + 2) = 2 * a (m + 1) - a m) : ∃ f : ℤ → ℤ, ∀ m, a m = f m   :=  by sorry