lean_workbook_plus_4705

Proved

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

Let $a^2 + b^2 = m$ and $ab = n$ ; then we must show $2(m^2 - n^2) \geq 3mn \Longleftrightarrow (2m + n)(m - 2n) \geq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4705 (m n : ℝ) : 2 * (m ^ 2 - n ^ 2) ≥ 3 * m * n ↔ (2 * m + n) * (m - 2 * n) ≥ 0   :=  by sorry

Source