src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Tue Oct 31 17:32:56 2023 +0100
+++ b/src/HOL/Nat.thy	Thu Nov 02 14:10:08 2023 +0000
@@ -342,7 +342,10 @@
 lemma Suc_diff_diff [simp]: "(Suc m - n) - Suc k = m - n - k"
   by (simp add: diff_diff_add)
 
-lemma diff_Suc_1 [simp]: "Suc n - 1 = n"
+lemma diff_Suc_1: "Suc n - 1 = n"
+  by simp
+
+lemma diff_Suc_1' [simp]: "Suc n - Suc 0 = n"
   by simp