# HG changeset patch
# User huffman
# Date 1163029392 -3600
# Node ID 62f25a96f0c1cf6f07aa0e226befe7b2782d26a2
# Parent  b7f090c5057de1f25ee398efd5ea4c117627dd03
added lemma mult_mono'

diff -r b7f090c5057d -r 62f25a96f0c1 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Thu Nov 09 00:19:16 2006 +0100
+++ b/src/HOL/Ring_and_Field.thy	Thu Nov 09 00:43:12 2006 +0100
@@ -510,6 +510,13 @@
 apply (erule mult_left_mono, assumption)
 done
 
+lemma mult_mono':
+     "[|a \<le> b; c \<le> d; 0 \<le> a; 0 \<le> c|] 
+      ==> a * c  \<le>  b * (d::'a::pordered_semiring)"
+apply (rule mult_mono)
+apply (fast intro: order_trans)+
+done
+
 lemma less_1_mult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::'a::ordered_semidom)"
 apply (insert mult_strict_mono [of 1 m 1 n]) 
 apply (simp add:  order_less_trans [OF zero_less_one])