lean_workbook_plus_56040

Proved

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

Prove that if $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_56040 {x y : ℝ} (h : y ≥ 0) (h' : y * (y + 1) ≤ (x + 1) ^ 2) : y * (y - 1) ≤ x ^ 2   :=  by sorry

Source