# HG changeset patch
# User haftmann
# Date 1235317716 -3600
# Node ID 7dc7b029b878d09869ebf24c750e36dce27dbe9d
# Parent  36d7d337510ef46264eb480db07e441b530436e1# Parent  044308b4948aaf2eb58822c3e70755cf1cbc1172
merged

diff -r 36d7d337510e -r 7dc7b029b878 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Feb 22 16:48:11 2009 +0100
+++ b/src/HOL/Divides.thy	Sun Feb 22 16:48:36 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")