lean_workbook_plus_31726

Proved

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

Show that for a real number $a \geq 1$ the inequality $\displaystyle a^5+a^4+a^3+a^2+a+1 \geq 2(a^2+a+1)$ holds.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_31726 (a : ℝ) (h : 1 ≤ a) : a^5 + a^4 + a^3 + a^2 + a + 1 ≥ 2 * (a^2 + a + 1)   :=  by sorry

Source