diff -r d4967d2188d6 -r a4c2a0ffa5be src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Thu Aug 30 17:09:02 2007 +0200
+++ b/src/HOL/IntDiv.thy	Thu Aug 30 21:43:08 2007 +0200
@@ -935,6 +935,19 @@
 apply (auto simp add: mult_commute)
 done
 
+lemma zmod_zmod_cancel:
+assumes "n dvd m" shows "(k::int) mod m mod n = k mod n"
+proof -
+  from `n dvd m` obtain r where "m = n*r" by(auto simp:dvd_def)
+  have "k mod n = (m * (k div m) + k mod m) mod n"
+    using zmod_zdiv_equality[of k m] by simp
+  also have "\<dots> = (m * (k div m) mod n + k mod m mod n) mod n"
+    by(subst zmod_zadd1_eq, rule refl)
+  also have "m * (k div m) mod n = 0" using `m = n*r`
+    by(simp add:mult_ac)
+  finally show ?thesis by simp
+qed
+
 
 subsection {*Splitting Rules for div and mod*}