Factorial with big operators

This file contains some lemmas on factorials in combination with big operators.

While in terms of semantics they could be in the Basic.lean file, importing Algebra.BigOperators.Group.Finset leads to a cyclic import.

theorem Nat.monotone_factorial : Monotone Nat.factorial

theorem Nat.prod_factorial_pos {α : Type u_1} (s : Finset α) (f : α → ℕ) : 0 < ∏ i ∈ s, (f i).factorial

theorem Nat.prod_factorial_dvd_factorial_sum {α : Type u_1} (s : Finset α) (f : α → ℕ) : ∏ i ∈ s, (f i).factorial ∣ (∑ i ∈ s, f i).factorial

theorem Nat.descFactorial_eq_prod_range (n : ℕ) (k : ℕ) : n.descFactorial k = ∏ i ∈ Finset.range k, (n - i)