lean_workbook_plus_75915

Disproved

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

Prove that $x^2-x+1\geq x^2-2x+1+\frac{4(x-1)}{x+1}+\frac{4}{(x+1)^2}=\left(x-1+\frac{2}{x+1}\right)^2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75915 : ∀ x : ℝ, x^2 - x + 1 ≥ x^2 - 2 * x + 1 + 4 * (x - 1) / (x + 1) + 4 / (x + 1)^2   :=  by sorry

Source