lean_workbook_plus_25516

Proved

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

Prove $4 x^6-3x^5+x^4+5x^3+2 x^2-x+1>0$ for $x > 0$ and $x \neq 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_25516 (x : ℝ) (hx : x > 0) (h'x : x ≠ 1) : 4 * x^6 - 3 * x^5 + x^4 + 5 * x^3 + 2 * x^2 - x + 1 > 0   :=  by sorry

Source