--- a/src/HOL/IntDiv.thy Thu Jan 08 08:24:08 2009 -0800
+++ b/src/HOL/IntDiv.thy Thu Jan 08 08:36:16 2009 -0800
@@ -938,18 +938,8 @@
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
+lemma zmod_zmod_cancel: "n dvd m \<Longrightarrow> (k::int) mod m mod n = k mod n"
+by (rule mod_mod_cancel)
subsection {*Splitting Rules for div and mod*}