lean_workbook_plus_9414

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_9414 {a : ℕ → ℝ} (a1 : a 0 = 1) (a_rec : ∀ n, a (n + 1) = (3 * (n + 1)) / ((n + 1 + 1) * (n + 1 + 2)) * a 1) : ∀ n, a n = (3 * n) / ((n + 1) * (n + 2)) * a 1   :=  by sorry