lean_workbook_plus_44232

Proved

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

Suffice it to prove for $b=c=1$ and $a\geq1$ i.e. $\frac{(a+1)^2}{a}\geq\frac{12(a^2+2)}{(a+2)^2}\Leftrightarrow (a-1)^2(a-2)^2\geq0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_44232 :  ∀ a : ℝ, 1 ≤ a → (a + 1) ^ 2 / a ≥ 12 * (a ^ 2 + 2) / (a + 2) ^ 2   :=  by sorry

Source