lean_workbook_plus_25330

Proved

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

Prove that $(x^{n+1}+1)^2\cdot (x+1)^2 \ge 4x(x^{n+2}+1)(x^n+1)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_25330 (x : ℝ) (n : ℕ) :
  (x^(n+1) + 1)^2 * (x + 1)^2 ≥ 4 * x * (x^(n+2) + 1) * (x^n + 1)   :=  by sorry

Source