theorem principle_of_induction (P : ℕ → Prop) (h₁ : P 1) (hstep : ∀ (n : ℕ), P n → P (n + 1)) (n : ℕ) : P (n + 1)

Theorem 0.3.6 (principle of induction). Let P : ℕ → Prop. If (i) the basis statement P 1 holds and (ii) the induction step says P n → P (n + 1) for each n, then P (n + 1) holds for every natural number n.

theorem pow_two_le_factorial_succ (n : ℕ) : 2 ^ n ≤ (n + 1).factorial

Example 0.3.7: For all natural numbers n, the inequality 2^(n - 1) ≤ n! holds, proved by induction on n.

theorem pow_two_pred_le_factorial (n : ℕ) : 2 ^ (n - 1) ≤ n.factorial

theorem rewrite_neg_ratio (c : ℝ) (m : ℕ) : (c ^ m - 1) / (c - 1) = (1 - c ^ m) / (1 - c)

Example 0.3.8: For any real c ≠ 1 and any natural number n, the finite geometric sum satisfies 1 + c + c^2 + ⋯ + c^n = (1 - c^(n+1)) / (1 - c).

theorem geometric_sum_closed_form {c : ℝ} (hc : c ≠ 1) (n : ℕ) : ∑ i ∈ Finset.range (n + 1), c ^ i = (1 - c ^ (n + 1)) / (1 - c)

theorem principle_of_strong_induction (P : ℕ → Prop) (h₁ : P 1) (hstep : ∀ (n : ℕ), (∀ (k : ℕ), 1 ≤ k → k ≤ n → P k) → P (n + 1)) (n : ℕ) : P (n + 1)

Theorem 0.3.9 (principle of strong induction). Let P : ℕ → Prop. (i) The basis statem/ent P 1 is true. (ii) If P k holds for all k = 1, 2, …, n, then P (n + 1) is true. Then P n holds for all natural numbers n.