diff -r 0aa2d1c132b2 -r 25dd3726fd00 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Feb 05 16:34:56 2025 +0000
+++ b/src/HOL/Nat.thy	Thu Feb 06 16:20:52 2025 +0000
@@ -1268,7 +1268,7 @@
 
 lemma diff_is_0_eq' [simp]: "m \<le> n \<Longrightarrow> m - n = 0"
   for m n :: nat
-  by (rule iffD2, rule diff_is_0_eq)
+  by simp
 
 lemma zero_less_diff [simp]: "0 < n - m \<longleftrightarrow> m < n"
   for m n :: nat
@@ -1755,6 +1755,9 @@
     by simp
 qed
 
+lemma of_nat_diff_if: \<open>of_nat (m - n) = (if n\<le>m then of_nat m - of_nat n else 0)\<close>
+  by (simp add: not_le less_imp_le)
+
 end
 
 text \<open>Class for unital semirings with characteristic zero.