feat: grind_pattern mod_eq_of_lt

src/Init/Data/Nat/Div/Basic.lean

@@ -179,6 +179,15 @@ theorem mod_eq_of_lt {a b : Nat} (h : a < b) : a % b = a :=
     if_neg h'
   (mod_eq a b).symm ▸ this
 
+grind_pattern mod_eq_of_lt => a % b where
+  not_value a
+  guard a < b
+
+grind_pattern mod_eq_of_lt => a % b where
+  not_value b
+  is_value a -- prevents overlaps with the above `grind_pattern`
+  guard a < b
+
 @[simp] theorem one_mod_eq_zero_iff {n : Nat} : 1 % n = 0 ↔ n = 1 := by
   match n with
   | 0 => simp