lean_workbook_plus_19017

Proved

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

Let x,y>0. Prove the inequality is true, \n\n $\frac{3}{2}x^2+\frac{3}{2}y^2+2xy-x-y+1 \ge (x+y)^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19017 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : 3/2 * x^2 + 3/2 * y^2 + 2 * x * y - x - y + 1 ≥ (x + y)^2   :=  by sorry

Source