# HG changeset patch
# User paulson
# Date 931855319 -7200
# Node ID 4e0defe58b4222214f3325351873ee927dddb8c8
# Parent  82a4ac9c6b039942ba8d6165f0ef8c0d7b5cb382
simplified the <= monotonicity proof

diff -r 82a4ac9c6b03 -r 4e0defe58b42 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Mon Jul 12 22:29:38 1999 +0200
+++ b/src/HOL/Arith.ML	Tue Jul 13 10:41:59 1999 +0200
@@ -516,13 +516,15 @@
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
 qed "mult_le_mono1";
 
-(*<=monotonicity, BOTH arguments*)
+Goal "i <= (j::nat) ==> k*i <= k*j";
+by (dtac mult_le_mono1 1);
+by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
+qed "mult_le_mono2";
+
+(* <= monotonicity, BOTH arguments*)
 Goal "[| i <= (j::nat); k <= l |] ==> i*k <= j*l";
 by (etac (mult_le_mono1 RS le_trans) 1);
-by (rtac le_trans 1);
-by (stac mult_commute 2);
-by (etac mult_le_mono1 2);
-by (simp_tac (simpset() addsimps [mult_commute]) 1);
+by (etac mult_le_mono2 1);
 qed "mult_le_mono";
 
 (*strict, in 1st argument; proof is by induction on k>0*)