lean_workbook_plus_67848

Proved

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

For any nonnegative reals $x, y$ show the inequality

x^2y^2 + x^2y + xy^2 \le x^3y^2 + x^2 + y^3

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67848 (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) : x^2*y^2 + x^2*y + x*y^2 ≤ x^3*y^2 + x^2 + y^3   :=  by sorry

Source