lean_workbook_plus_22842

Proved

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

Prove that $(x+1)^8>x^8+x^7-x^5-x^4-x^3+x+1$ for all $x\geq 2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_22842 : ∀ x ≥ 2, (x+1)^8 > x^8 + x^7 - x^5 - x^4 - x^3 + x + 1   :=  by sorry

Source