lean_workbook_plus_76098

Proved

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

Let $a$ be real number such that $-1\le a\le 1$ . Prove that: \n $(1+|a|+a^2)^3\geq (1+|a|)^3(1+|a|^3)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_76098 : ∀ a : ℝ, -1 ≤ a ∧ a ≤ 1 → (1 + |a| + a^2)^3 ≥ (1 + |a|)^3 * (1 + |a|^3)   :=  by sorry

Source