`BookProof.ChapterBijectionProbability.factorial_succ_le` (n : ℕ) : (n + 1)! ≤ (n + 1) ^ n

Initializing...

`BookProof.ChapterBijectionProbability.factorial_succ_le` (n : ℕ) : (n + 1)! ≤ (n + 1) ^ n · Prove2Me