α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ ↑r ! * ↑(choose n r) ≤ ↑(n ^ r)

α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ 0 < ↑r !
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ ↑(choose n r) ≤ ↑(n ^ r) / ↑r !
rw [le_div_iff']
no goals
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ 0 < ↑r !
exact_mod_cast r.factorial_pos
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ r ! * choose n r ≤ n ^ r
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ ↑r ! * ↑(choose n r) ≤ ↑(n ^ r)
norm_cast
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ descFactorial n r ≤ n ^ r
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ r ! * choose n r ≤ n ^ r
rw [← Nat.descFactorial_eq_factorial_mul_choose]
no goals
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ descFactorial n r ≤ n ^ r
exact n.descFactorial_le_pow r