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.Basic leads to a cyclic import.

theorem Nat.monotone_factorial : Monotone Nat.factorial

theorem Nat.prod_factorial_pos {α : Type u_1} (s : Finset α) (f : α → ℕ) : 0 < s.prod fun (i : α) => (f i).factorial

theorem Nat.prod_factorial_dvd_factorial_sum {α : Type u_1} (s : Finset α) (f : α → ℕ) : (s.prod fun (i : α) => (f i).factorial) ∣ (s.sum fun (i : α) => f i).factorial

theorem Nat.descFactorial_eq_prod_range (n : ℕ) (k : ℕ) : n.descFactorial k = (Finset.range k).prod fun (i : ℕ) => n - i