# HG changeset patch
# User nipkow
# Date 1235298641 -3600
# Node ID 410fefc247aa6d6c86721a0a005f098f5d9f3506
# Parent  6cf1fe60ac7352e7299ac049426a46c733ec9505
added dvd_div_mult

diff -r 6cf1fe60ac73 -r 410fefc247aa src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Feb 22 09:52:49 2009 +0100
+++ b/src/HOL/Divides.thy	Sun Feb 22 11:30:41 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")