fix: missing Nat div and mod norm rules in grind (#7512)

This PR adds missing normalization rules for `Nat` div and mod to the
`grind` tactic.

src/Init/Grind/Norm.lean

@@ -71,6 +71,12 @@ theorem beq_eq_decide_eq {_ : BEq α} [LawfulBEq α] [DecidableEq α] (a b : α)
 theorem bne_eq_decide_not_eq {_ : BEq α} [LawfulBEq α] [DecidableEq α] (a b : α) : (a != b) = (decide (¬ a = b)) := by
   by_cases a = b <;> simp [*]
 
+theorem natCast_div (a b : Nat) : (↑(a / b) : Int) = ↑a / ↑b := by
+  rfl
+
+theorem natCast_mod (a b : Nat) : (↑(a % b) : Int) = ↑a % ↑b := by
+  rfl
+
 init_grind_norm
   /- Pre theorems -/
   not_and not_or not_ite not_forall not_exists
@@ -114,19 +120,15 @@ init_grind_norm
   Bool.not_eq_true Bool.not_eq_false
   -- decide
   decide_eq_true_eq decide_not not_decide_eq_true
-  -- Nat LE
-  Nat.le_zero_eq
-  -- Nat/Int LT
-  Nat.lt_eq
-  -- Nat.succ
-  Nat.succ_eq_add_one
-  -- Nat op folding
+  -- Nat
+  Nat.le_zero_eq Nat.lt_eq Nat.succ_eq_add_one
   Nat.add_eq Nat.sub_eq Nat.mul_eq Nat.zero_eq Nat.le_eq
+  Nat.div_zero Nat.mod_zero
   -- Int
   Int.lt_eq
   Int.emod_neg Int.ediv_zero Int.emod_zero
   Int.natCast_add Int.natCast_mul Int.natCast_pow
-  Int.natCast_succ Int.natCast_zero
+  Int.natCast_succ Int.natCast_zero natCast_div natCast_mod
   -- GT GE
   ge_eq gt_eq
   -- Int op folding

tests/lean/run/grind_cutsat_nat_eq.lean

@@ -47,3 +47,11 @@ example (x y : Nat) : x + y - x = y := by
 
 example (x y : Nat) : (x - y) - y = x - 2*y := by
   grind
+
+example (x : Nat) : x / 0 = 0 := by
+  grind
+
+example (x : Nat) : x % 0 = x := by
+  grind
+
+example (x : Nat) : x % 4 - x % 8 = 0 := by grind