Recursive Sequence Bound

Let $a$ be sequence of real numbers such that $a_0 > 0$ and for all natural $n$, $$a_{n + 1} = a_{n} + \frac{n + 1}{a_n}.$$ Show that there exists a real number $c$ such that for all natural $n$, $$a_n \le n + 1 + \frac{c}{n + 1}.$$

Replace sorry in the template below with your solution. The Mathlib version currently used is v4.26.0.

import Mathlib.Data.Real.Basic

theorem solution (a : ℕ → ℝ) (ha_1 : 0 < a 0) (ha_rec : ∀ n : ℕ, a (n+1) = a n + (n + 1) / a n) :
    ∃ c : ℝ , ∀ n : ℕ, a n ≤ (n + 1) + c / (n + 1) := sorry

Login to submit a solution.