src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Tue Feb 24 11:12:58 2009 -0800
+++ b/src/HOL/Nat.thy	Wed Feb 25 06:53:15 2009 -0800
@@ -280,6 +280,9 @@
 lemma diff_add_0: "n - (n + m) = (0::nat)"
   by (induct n) simp_all
 
+lemma diff_Suc_1 [simp]: "Suc n - 1 = n"
+  unfolding One_nat_def by simp
+
 text {* Difference distributes over multiplication *}
 
 lemma diff_mult_distrib: "((m::nat) - n) * k = (m * k) - (n * k)"