lean_workbook_plus_61566

Proved

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

Given x,y are real number such that $x+y\ge 1$ and $|xy|\le 2$ . Prove $x^3+y^3\ge -7$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_61566 (x y : ℝ) (h1 : x + y ≥ 1) (h2 : |x*y| ≤ 2) : x^3 + y^3 ≥ -7   :=  by sorry

Source