lean_workbook_plus_8298

Proved

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

prove that : \n\n $(x-1)^2(x^2+1)\left(3\left[x+\frac{5}{6}\right]^2+\frac{11}{12}\right) \geq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8298 : ∀ x : ℝ, (x - 1) ^ 2 * (x ^ 2 + 1) * (3 * (x + 5 / 6) ^ 2 + 11 / 12) ≥ 0   :=  by sorry

Source