# HG changeset patch
# User huffman
# Date 1235573595 28800
# Node ID ecb557b021b245d24ac797c0396ac562094b06f3
# Parent  43c5b7bfc791e29d781e5c7ecd08613c6564268e
add lemma diff_Suc_1

diff -r 43c5b7bfc791 -r ecb557b021b2 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)"