theorem DerangementLowerBound.derangement_nat_ineq (n : ℕ) (hn : 1 ≤ n) : numDerangements n * n ^ n ≥ (n - 1) ^ n * n.factorial

Integer form of the derangement lower bound: for $n \ge 1$, $D_n \cdot n^n \ge (n-1)^n \cdot n!$, where $D_n = $ numDerangements n.

theorem DerangementLowerBound.derangement_lower_bound (n : ℕ) (hn : 1 ≤ n) : ↑(numDerangements n) / ↑n.factorial ≥ (1 - 1 / ↑n) ^ n

Corollary 6.5.6. The probability that a uniformly random permutation of $\{1, \dots, n\}$ has no fixed points is at least $(1 - 1/n)^n$.