lean_workbook_plus_12201

Proved

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

prove that $(t-2)\left[2t^{2}(t-2)+5t\left(t^{2}-4\right)+t^{3}+t+6\right]\ge 0$ for any $t\ge 2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_12201 (t : ℝ) (h₀ : 2 ≤ t) : (t - 2) * (2 * t ^ 2 * (t - 2) + 5 * t * (t ^ 2 - 4) + t ^ 3 + t + 6) ≥ 0   :=  by sorry

Source