lean_workbook_plus_81507

Proved

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

It is sufficient that: \n $12p-p^3\ge 27p-(p^2+3)(p+3)\Leftrightarrow 3p^2-12p+9\ge 0\Leftrightarrow 3(p-1)(p-3)\ge 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81507 : ∀ p : ℝ, 12 * p - p ^ 3 ≥ 27 * p - (p ^ 2 + 3) * (p + 3) ↔ 3 * (p - 1) * (p - 3) ≥ 0   :=  by sorry

Source