A two-variable polynomial inequality on the nonnegative quadrant

Proved

WorkbookSource.base_12960

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

lean-workbooksource-checked

Let be $x,y\ge 0$ . Prove that : $8x^3y+y^3+2x\ge 2xy(2x+y+1)$

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

Preamble

import Mathlib
open Real Nat

Formal statement

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

Source