lean_workbook_plus_55522

Proved

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

Prove that $x^{12}-x^{9}+x^4-x+1 > 0$ for $x \geq 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_55522 (x : ℝ) (hx : 1 ≤ x) : x ^ 12 - x ^ 9 + x ^ 4 - x + 1 > 0   :=  by sorry

Source