lean_workbook_plus_63048

Proved

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

Prove: $(1+p)^n \ge 1+np$ For every number $p>-1$ and for any positive integer $n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_63048 {p : ℝ} (hp : p > -1) {n : ℕ} (hn : n ≥ 1) : (1 + p)^n ≥ 1 + n * p   :=  by sorry

Source