lean_workbook_plus_78086

Proved

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

Prove or disprove: If $x$ and $y$ are real numbers with $y\geq0$ 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_78086 (x y : ℝ) (hy : 0 ≤ y) (h : y * (y + 1) ≤ (x + 1) ^ 2) : y * (y - 1) ≤ x ^ 2   :=  by sorry

Source