# 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 \ (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 \ (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 \ a dvd c \ (b div a dvd c div a) = (b dvd c)" apply (cases "a = 0")