Prove2Me

lean_workbook_plus_51768

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that 1a−1−1a+n+1(a+n+1)2≤1a−1−1a+n+1⇔(a+n+2)(a+n)≤(a+n+1)2\frac{1}{a-1}-\frac{1}{a+n}+\frac{1}{{{(a+n+1)}^{2}}}\le \frac{1}{a-1}-\frac{1}{a+n+1}\Leftrightarrow (a+n+2)(a+n)\le {{(a+n+1)}^{2}}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_51768  (a n : ℝ)
  (h₀ : 1 < a)
  (h₁ : 0 < n) :
  1 / (a - 1) - 1 / (a + n) + 1 / (a + n + 1)^2 ≤ 1 / (a - 1) - 1 / (a + n + 1) ↔ (a + n + 2) * (a + n) ≤ (a + n + 1)^2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph