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

α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ 0 < ↑r !
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ ↑((n + 1 - r) ^ r) / ↑r ! ≤ ↑(choose n r)
rw [div_le_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 : ℕ
⊢ (n + 1 - r) ^ r ≤ r ! * choose n r
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ ↑((n + 1 - r) ^ r) ≤ ↑r ! * ↑(choose n r)
norm_cast
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ (n + 1 - r) ^ r ≤ descFactorial n r
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ (n + 1 - r) ^ r ≤ r ! * choose n r
rw [← Nat.descFactorial_eq_factorial_mul_choose]
no goals
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ (n + 1 - r) ^ r ≤ descFactorial n r
exact n.pow_sub_le_descFactorial r