Prime natural numbers and the factorial operator

theorem Nat.Prime.dvd_factorial {n p : ℕ} : Prime p → (p ∣ n.factorial ↔ p ≤ n)

theorem Nat.coprime_factorial_iff {m n : ℕ} (hm : m ≠ 1) : m.Coprime n.factorial ↔ n < m.minFac

theorem Nat.Prime.coprime_factorial_of_lt {p n : ℕ} (hp : Prime p) (hn : n < p) : p.Coprime n.factorial

theorem Nat.Prime.coprime_descFactorial_of_lt_of_le {p n k : ℕ} (hp : Prime p) (hn : n < p) (hk : k ≤ n) : p.Coprime (n.descFactorial k)