src/HOL/Divides.ML

 by (case_tac "k<n" 1);
 by (ALLGOALS (asm_simp_tac(simpset() addsimps ([add_assoc] @
                        [mod_less, mod_geq, div_less, div_geq,
                         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])));
 qed "div_1";