lean_workbook_plus_12962

Proved

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

Prove that the inequality $125b(3-b)+\dfrac {(3-b)^2(125b+\dfrac{525} 2)} 4\le 666$ holds for $b\le 3$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_12962 (b : ℝ) (hb : b ≤ 3) :
  125 * b * (3 - b) + (3 - b) ^ 2 * (125 * b + 525 / 2) / 4 ≤ 666   :=  by sorry

Source