--- a/src/HOL/Nat.thy	Sun May 05 15:31:08 2024 +0100
+++ b/src/HOL/Nat.thy	Mon May 06 14:39:33 2024 +0100
@@ -1752,7 +1752,7 @@
 context semiring_1_cancel
 begin
 
-lemma of_nat_diff:
+lemma of_nat_diff [simp]:
   \<open>of_nat (m - n) = of_nat m - of_nat n\<close> if \<open>n \<le> m\<close>
 proof -
   from that obtain q where \<open>m = n + q\<close>