lean_workbook_plus_53578

Proved

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

x between 0,1 $x^8+x^2<1$ , $x^5+x<1$ , so $1 \geq x^5+x-x^8-x^2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_53578 : ∀ x : ℝ, x ∈ Set.Icc 0 1 → x^5 + x - x^8 - x^2 ≤ 1   :=  by sorry

Source