chore: add test to keep powering in ZMod fast (#17996)

Thanks to #8885 we can now evaluate powers in `ZMod M` much more efficiently for large `M`. To guard against reversion, we add a test that for a chosen 1024-bit prime and base we should satisfy Fermat's Little Theorem when `#eval` is used.

test/BinPow.lean

@@ -0,0 +1,13 @@
+import Mathlib.Data.ZMod.Defs
+
+-- A 1024-bit prime number
+set_option linter.style.longLine false in
+abbrev M : Nat := 0xb10b8f96a080e01dde92de5eae5d54ec52c99fbcfb06a3c69a6a9dca52d23b616073e28675a23d189838ef1e2ee652c013ecb4aea906112324975c3cd49b83bfaccbdd7d90c4bd7098488e9c219a73724effd6fae5644738faa31a4ff55bccc0a151af5f0dc8b4bd45bf37df365c1a65e68cfda76d4da708df1fb2bc2e4a4371
+
+set_option linter.style.longLine false in
+abbrev g : Nat := 0xa4d1cbd5c3fd34126765a442efb99905f8104dd258ac507fd6406cff14266d31266fea1e5c41564b777e690f5504f213160217b4b01b886a5e91547f9e2749f4d7fbd7d3b9a92ee1909d0d2263f80a76a6a24c087a091f531dbf0a0169b6a28ad662a4d18e73afa32d779d5918d08bc8858f4dcef97c2a24855e6eeb22b3b2e5
+
+-- This should evaluate within a few seconds compared to never(ish) previously
+/-- info: 1 -/
+#guard_msgs in
+#eval (g : ZMod M) ^ (M - 1)