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