Prime natural numbers and the factorial operator

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