# HG changeset patch
# User paulson
# Date 893764241 -7200
# Node ID a7322db15065bbc369601cbc19791e71a1de3083
# Parent  196100237656bb493e71b5d82e2ba122cbeb810c
new thm mult_lt_mono1

diff -r 196100237656 -r a7322db15065 src/ZF/Arith.ML
--- a/src/ZF/Arith.ML	Mon Apr 27 19:32:19 1998 +0200
+++ b/src/ZF/Arith.ML	Tue Apr 28 13:50:41 1998 +0200
@@ -532,6 +532,10 @@
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono])));
 qed "mult_lt_mono2";
 
+goal thy "!!k. [| i<j; 0<k; i:nat; j:nat; k:nat |] ==> i#*k < j#*k";
+by (asm_simp_tac (simpset() addsimps [mult_lt_mono2, mult_commute]) 1);
+qed "mult_lt_mono1";
+
 goal Arith.thy "!!k. [| m: nat; n: nat |] ==> 0 < m#*n <-> 0<m & 0<n";
 by (best_tac (claset() addEs [natE] addss (simpset())) 1);
 qed "zero_lt_mult_iff";