# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1698934208 0
# Node ID fb6828831ef1bc1c57ede4624ef08f02bd076f6b
# Parent  711acefe97a39359cbc3c9c21561000fec211e0b
fixed the simplification of Suc n - 1

diff -r 711acefe97a3 -r fb6828831ef1 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