From 8a79ef36331e7dd7e757cc3a14717ef931f3cd40 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 19 Sep 2025 11:50:39 -0700
Subject: [PATCH] chore: missing `grind` normalization (#10463)

This PR adds `Nat.sub_zero` as a `grind` normalization rule.
---
 src/Init/Grind/Norm.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Grind/Norm.lean b/src/Init/Grind/Norm.lean
index 53a2206018..d535f1d337 100644
--- a/src/Init/Grind/Norm.lean
+++ b/src/Init/Grind/Norm.lean
@@ -182,7 +182,7 @@ init_grind_norm
   Nat.add_eq Nat.sub_eq Nat.mul_eq Nat.zero_eq Nat.le_eq
   Nat.div_zero Nat.mod_zero Nat.div_one Nat.mod_one
   Nat.sub_sub Nat.pow_zero Nat.pow_one Nat.sub_self
-  Nat.one_pow Nat.zero_sub
+  Nat.one_pow Nat.zero_sub Nat.sub_zero
   -- Int
   Int.lt_eq
   Int.emod_neg Int.ediv_neg