diff --git a/src/Init/Data/Nat/Div/Basic.lean b/src/Init/Data/Nat/Div/Basic.lean
index 2e24e47375..311039aac1 100644
--- a/src/Init/Data/Nat/Div/Basic.lean
+++ b/src/Init/Data/Nat/Div/Basic.lean
@@ -39,7 +39,7 @@ Examples:
  * `0 / 22 = 0`
  * `5 / 0 = 0`
 -/
-@[extern "lean_nat_div"]
+@[extern "lean_nat_div", irreducible]
 protected def div (x y : @& Nat) : Nat :=
   if hy : 0 < y then
     let rec
@@ -140,7 +140,7 @@ reductions](lean-manual://section/type-system) when the `Nat`s contain free vari
 This function is overridden at runtime with an efficient implementation. This definition is the
 logical model.
 -/
-@[extern "lean_nat_mod"]
+@[extern "lean_nat_mod", irreducible]
 protected noncomputable def modCore (x y : Nat) : Nat :=
   if hy : 0 < y then
     let rec
diff --git a/tests/lean/run/7612.lean b/tests/lean/run/7612.lean
new file mode 100644
index 0000000000..4cf4966315
--- /dev/null
+++ b/tests/lean/run/7612.lean
@@ -0,0 +1,5 @@
+
+theorem extracted_1 (x y : BitVec 9) :
+    (y - y.srem x).sdiv x = y.sdiv x := by
+  ac_nf
+  sorry