lean_workbook_plus_39772

Proved

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

Prove or disprove using the AM-GM inequality: If x and y are real numbers with $y\geq 0$ and $y(y+1)\leq (x+1)^{2}$ , then $y(y-1)\leq x^{2}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_39772 : ∀ x y : ℝ, y ≥ 0 ∧ y * (y + 1) ≤ (x + 1) ^ 2 → y * (y - 1) ≤ x ^ 2   :=  by sorry

Source