`BookProof.ChapterBijectionProbability.factorial_succ_le` (n : ℕ) : (n + 1)! ≤ (n + 1) ^ n
ProvedBookProof.ChapterBijectionProbability.factorial_succ_letheoremstimepiece
Prove the following Lean 4 theorem from ChapterBijectionProbability.
BookProof.ChapterBijectionProbability.factorial_succ_le (n : ℕ) : (n + 1)! ≤ (n + 1) ^ n
Formalization note: Lean 4 identifier BookProof.ChapterBijectionProbability.factorial_succ_le.
Preamble
-- Generated from ChapterBijectionProbability.lean — theorem BookProof.ChapterBijectionProbability.factorial_succ_le import Mathlib import Definitions.Def_ChapterBijectionProbability open BookProof.ChapterBijectionProbability open scoped Nat open Filter Asymptotics
Formal statement
theorem BookProof.ChapterBijectionProbability.factorial_succ_le (n : ℕ) : (n + 1)! ≤ (n + 1) ^ n := by sorry