Add test for mod_eq_of_lt grind annotation

Author: pirapira

tests/playground/div_mod_grind.lean

@@ -0,0 +1,11 @@
+import Init.Data.Nat.Div.Basic
+
+-- Uncommenting this repetition enables `grind` to solve the example:
+-- grind_pattern Nat.mod_eq_of_lt => a % b where
+--   guard (a < b)
+
+-- The same command is already in Init.Data.Nat.Div.Basic
+
+example : (a : Nat) < b → a % b = a := by
+  set_option trace.grind.debug.ematch true in
+  grind