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