lean_workbook_plus_17679

Proved

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

Prove that for every $p>=1$ the Inequality Is true \n\n $2p^3 + 4p + 1 >=6p^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17679 (p : ℝ) (hp : 1 ≤ p) : 2 * p ^ 3 + 4 * p + 1 ≥ 6 * p ^ 2   :=  by sorry

Source