lean_workbook_plus_66593

Proved

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

It remains to prove that $32a^{5}+32a^{4}-16a^{3}-16a^{2}+9a-1 \ge 0$ for all $1 \ge a \ge \frac{1}{5}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_66593 (a : ℝ) (ha1 : 1 ≥ a ∧ a ≥ 1/5) : 32*a^5 + 32*a^4 - 16*a^3 - 16*a^2 + 9*a - 1 ≥ 0   :=  by sorry

Source