# HG changeset patch
# User nipkow
# Date 1235298657 -3600
# Node ID 044308b4948aaf2eb58822c3e70755cf1cbc1172
# Parent  a416ed407f823c2b9307268cd91030372ac88257# Parent  410fefc247aa6d6c86721a0a005f098f5d9f3506
merged

diff -r a416ed407f82 -r 044308b4948a src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Feb 22 10:22:46 2009 +0100
+++ b/src/HOL/Divides.thy	Sun Feb 22 11:30:57 2009 +0100
@@ -178,6 +178,12 @@
 lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b"
 by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0)
 
+lemma dvd_div_mult: "a dvd b \<Longrightarrow> (b div a) * c = b * c div a"
+apply (cases "a = 0")
+ apply simp
+apply (auto simp: dvd_def mult_assoc)
+done
+
 lemma div_dvd_div[simp]:
   "a dvd b \<Longrightarrow> a dvd c \<Longrightarrow> (b div a dvd c div a) = (b dvd c)"
 apply (cases "a = 0")