A quadratic bound from a cubic inequality

Proved

WorkbookSource.problem_2101

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

inequalitieslean-workbooksource-checked

If $x,y>0$ and $x^3+y^3\le x-y$ , then $x^2+y^2\le1$ .

Source: InternLM Lean-Workbook, record lean_workbook_2101 (Apache-2.0). The complete source proposition is preserved.

Preamble

import Mathlib

Formal statement

theorem WorkbookSource.problem_2101 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) (h : x^3 + y^3 ≤ x - y) : x^2 + y^2 ≤ 1  :=  by sorry

Source