lean_workbook_plus_30443

Proved

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

Given $x \ge 0$ , prove that $\frac{(x^2 + 1)^6}{2^7}+\frac12 \ge x^5 - x^3 + x$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_30443 (x : ℝ) (hx : 0 ≤ x) : (x^2 + 1)^6 / 2^7 + 1 / 2 ≥ x^5 - x^3 + x   :=  by sorry

Source