chore: split Data.Num.Lemmas (#23655)

I have taken out a large block of statements (and a few tactics) that use `ZNum` or rely on statements that use `ZNum` and put them into `Data.Num.ZNum`.

Author: Parcly-Taxel

Mathlib.lean

@@ -3158,6 +3158,7 @@ import Mathlib.Data.Num.Basic
 import Mathlib.Data.Num.Bitwise
 import Mathlib.Data.Num.Lemmas
 import Mathlib.Data.Num.Prime
+import Mathlib.Data.Num.ZNum
 import Mathlib.Data.Opposite
 import Mathlib.Data.Option.Basic
 import Mathlib.Data.Option.Defs