A two-variable quartic inequality with lower-degree terms

Proved

WorkbookSource.base_21393

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

lean-workbooksource-checked

Let $x,y>0$ .Prove that ${{x}^{3}}y+x{{y}^{3}}+1\ge x{{y}^{2}}+{{x}^{2}}y+xy.$

Source: InternLM Lean-Workbook, record lean_workbook_21393 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_21393 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : x^3 * y + x * y^3 + 1 ≥ x^2 * y + x * y^2 + x * y  :=  by sorry

Source