lean_workbook_plus_54755

Proved

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

Prove that for real $y\ge-1$ and integers $k\ge1$ we have $(y+1)^k\ge ky+1$ . And equality holds if and only if $y=0$ or $k=1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_54755 (y : ℝ) (k : ℕ) (_hk : 1 ≤ k) (_hy : -1 ≤ y) : (y + 1) ^ k ≥ k * y + 1   :=  by sorry

Source