fix: change the proof of Nat.zero_mod to rfl (#9391)

This PR replaces the proof of the simplification lemma `Nat.zero_mod`
with
`rfl` since it is, by design, a definitional equality. This solves an
issue
whereby the lemma could not be used by the simplifier when in 'dsimp'
mode.

Closes #9389

---------

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

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

@@ -350,12 +350,7 @@ theorem mod_le (x y : Nat) : x % y ≤ x := by
 theorem mod_lt_of_lt {a b c : Nat} (h : a < c) : a % b < c :=
   Nat.lt_of_le_of_lt (Nat.mod_le _ _) h
 
-@[simp] theorem zero_mod (b : Nat) : 0 % b = 0 := by
-  rw [mod_eq]
-  have : ¬ (0 < b ∧ b = 0) := by
-    intro ⟨h₁, h₂⟩
-    simp_all
-  simp [this]
+@[simp] theorem zero_mod (b : Nat) : 0 % b = 0 := rfl
 
 @[simp] theorem mod_self (n : Nat) : n % n = 0 := by
   rw [mod_eq_sub_mod (Nat.le_refl _), Nat.sub_self, zero_mod]

tests/lean/run/9389.lean

@@ -0,0 +1,2 @@
+/-! Tests that `zero_mod` is `@[defeq]` -/
+example (n : Nat) : 0 % n = 0 := by dsimp