Theorem: Nat.choose_le_pow' (ExponentialRamsey/Prereq/Mathlib/Analysis/SpecialFunctions/ExplicitStirling.lean)

State before:
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ ↑(choose n r) ≤ ↑n ^ r / ↑r !
Tactic:
simpa using Nat.choose_le_pow (α := α) r n
State after:
no goals