add lemma diff_Suc_1
authorhuffman
Wed Feb 25 06:53:15 2009 -0800 (2009-02-25)
changeset 30093ecb557b021b2
parent 30082 43c5b7bfc791
child 30094 83e864eb239f
add lemma diff_Suc_1
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Nat.thy	Tue Feb 24 11:12:58 2009 -0800
     1.2 +++ b/src/HOL/Nat.thy	Wed Feb 25 06:53:15 2009 -0800
     1.3 @@ -280,6 +280,9 @@
     1.4  lemma diff_add_0: "n - (n + m) = (0::nat)"
     1.5    by (induct n) simp_all
     1.6  
     1.7 +lemma diff_Suc_1 [simp]: "Suc n - 1 = n"
     1.8 +  unfolding One_nat_def by simp
     1.9 +
    1.10  text {* Difference distributes over multiplication *}
    1.11  
    1.12  lemma diff_mult_distrib: "((m::nat) - n) * k = (m * k) - (n * k)"