feat: port data.nat.prime (#1156)

- [x] depends on #1142

Co-authored-by: ART0 <18333981+0Art0@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: 3 people

Mathlib.lean

@@ -231,6 +231,7 @@ import Mathlib.Data.Nat.Order.Basic
 import Mathlib.Data.Nat.Order.Lemmas
 import Mathlib.Data.Nat.PSub
 import Mathlib.Data.Nat.Pow
+import Mathlib.Data.Nat.Prime
 import Mathlib.Data.Nat.Set
 import Mathlib.Data.Nat.Size
 import Mathlib.Data.Nat.Sqrt