author | huffman |
Wed, 25 Feb 2009 06:53:15 -0800 | |
changeset 30093 | ecb557b021b2 |
parent 30082 | 43c5b7bfc791 |
child 30094 | 83e864eb239f |
src/HOL/Nat.thy | file | annotate | diff | comparison | revisions |
--- 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)"