# HG changeset patch
# User paulson
# Date 994166969 -7200
# Node ID 48fc0db9b896f03933a5fe9e226aedb3dcebbb17
# Parent  2eeaa1077b7373a65ddcfc0c68b3c8e7b540c5ed
new lemmas

diff -r 2eeaa1077b73 -r 48fc0db9b896 src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Tue Jul 03 15:29:17 2001 +0200
+++ b/src/HOL/Divides.ML	Tue Jul 03 15:29:29 2001 +0200
@@ -613,6 +613,18 @@
 by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
 qed "dvd_mult_cancel";
 
+Goal "0<m ==> (m*n dvd m) = (n=1)";
+by Auto_tac;  
+by (subgoal_tac "m*n dvd m*1" 1);
+by (dtac dvd_mult_cancel 1); 
+by Auto_tac;  
+qed "dvd_mult_cancel1";
+
+Goal "0<m ==> (n*m dvd m) = (n=1)";
+by (stac mult_commute 1); 
+by (etac dvd_mult_cancel1 1); 
+qed "dvd_mult_cancel2";
+
 Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)";
 by (Clarify_tac 1);
 by (res_inst_tac [("x","k*ka")] exI 1);