# HG changeset patch
# User nipkow
# Date 881222739 -3600
# Node ID aa22fcb46a5d2d04bdd615d4f06b44bc1d205f6e
# Parent  b852e2d2a39a6e6b4d0a874b512df1dcf95addbb
Added thm mult_div_cancel

diff -r b852e2d2a39a -r aa22fcb46a5d src/HOL/Divides.ML
--- 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])));