# HG changeset patch
# User paulson
# Date 930817977 -7200
# Node ID 32b5d68196d27f165a4fdc287b42e8335af0d170
# Parent  6c8bf18f9da9921b449aef3af22179f3e1d3cf52
new laws mult_le_cancel1, mult_le_cancel2

diff -r 6c8bf18f9da9 -r 32b5d68196d2 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Wed Jun 30 16:00:06 1999 +0200
+++ b/src/HOL/Arith.ML	Thu Jul 01 10:32:57 1999 +0200
@@ -566,6 +566,15 @@
 qed "mult_less_cancel1";
 Addsimps [mult_less_cancel1, mult_less_cancel2];
 
+Goal "0<k ==> (m*k <= n*k) = (m<=n)";
+by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
+qed "mult_le_cancel2";
+
+Goal "0<k ==> (k*m <= k*n) = (m<=n)";
+by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
+qed "mult_le_cancel1";
+Addsimps [mult_le_cancel1, mult_le_cancel2];
+
 Goal "(Suc k * m < Suc k * n) = (m < n)";
 by (rtac mult_less_cancel1 1);
 by (Simp_tac 1);