lean_workbook_plus_49163
ProvedProve that the sequence is increasing.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_49163 (f : ℕ → ℝ) (n m : ℕ) (h₁ : m > n) (h₂ : f m = (2 * m + 1) / (m + 1)) (h₃ : f n = (2 * n + 1) / (n + 1)) : f m > f n := by sorry
Source