lean_workbook_plus_18321

Proved

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

Let $x, y$ are real numbers such that $x + y \geq 0.$ Prove that $x ^ 5 + y ^ 5\geq xy(x^3 +y^ 3)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_18321 (x y : ℝ) (h : x + y ≥ 0) : x ^ 5 + y ^ 5 ≥ x * y * (x ^ 3 + y ^ 3)   :=  by sorry

Source