lean_workbook_plus_3110

Proved

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

For real and positive numbers $x,y$ which satisfy $x^3+y^3 = x-y$ , prove that $x^2 + y^2 < 1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_3110 (x y : ℝ) (h1 : 0 < x ∧ 0 < y) (h2 : x^3 + y^3 = x - y) : x^2 + y^2 < 1   :=  by sorry

Source