Added thm mult_div_cancel

--- a/src/HOL/Divides.ML	Wed Dec 03 17:31:25 1997 +0100
+++ b/src/HOL/Divides.ML	Thu Dec 04 09:05:39 1997 +0100
@@ -108,6 +108,13 @@
                         add_diff_inverse, diff_less]))));
 qed "mod_div_equality";
 
+(* a simple rearrangement of mod_div_equality: *)
+goal thy "!!k. 0<k ==> k*(m div k) = m - (m mod k)";
+by(dres_inst_tac [("m","m")] mod_div_equality 1);
+by (EVERY1[etac subst, simp_tac (simpset() addsimps mult_ac),
+           K(IF_UNSOLVED no_tac)]);
+qed "mult_div_cancel";
+
 goal thy "m div 1 = m";
 by (induct_tac "m" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_less, div_geq])));