lean_workbook_plus_71351

Proved

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

Let $a+b=2u$ and $ab=v^2,$ where $v>0$ . Prove that $a^2b^2(a^2+b^2-2)\geq (a+b)(ab-1)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_71351 {a b u v : ℝ} (ha : a > 0) (hb : b > 0) (hv : v > 0) (hab : a + b = 2 * u) (h : a * b = v ^ 2) : a ^ 2 * b ^ 2 * (a ^ 2 + b ^ 2 - 2) ≥ (a + b) * (a * b - 1)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph