lean_workbook_plus_18969

Proved

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

Use : $y^6+z^6-yz(y^4+z^4)=(y-z)(y^5-z^5) \ge 0 \rightarrow y^6+z^6 \ge yz(y^4+z^4)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_18969 : ∀ y z : ℝ, y^6 + z^6 ≥ y * z * (y^4 + z^4)   :=  by sorry

Source