# HG changeset patch
# User haftmann
# Date 1423905855 -3600
# Node ID 7f2b60cb5190642175dd26ffbc5b9d826ac0fecd
# Parent  03bde055a1a04535c40016aecec09875f6ccacf0
fact consolidation

diff -r 03bde055a1a0 -r 7f2b60cb5190 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sat Feb 14 10:24:15 2015 +0100
+++ b/src/HOL/Rings.thy	Sat Feb 14 10:24:15 2015 +0100
@@ -719,24 +719,14 @@
   done
 
 lemma mult_less_imp_less_left:
-  assumes less: "c * a < c * b" and nonneg: "0 \<le> c"
+  assumes "c * a < c * b" and "0 \<le> c"
   shows "a < b"
-proof (rule ccontr)
-  assume "\<not>  a < b"
-  hence "b \<le> a" by (simp add: linorder_not_less)
-  hence "c * b \<le> c * a" using nonneg by (rule mult_left_mono)
-  with this and less show False by (simp add: not_less [symmetric])
-qed
+  using assms by (fact mult_left_less_imp_less)
 
 lemma mult_less_imp_less_right:
   assumes less: "a * c < b * c" and nonneg: "0 \<le> c"
   shows "a < b"
-proof (rule ccontr)
-  assume "\<not> a < b"
-  hence "b \<le> a" by (simp add: linorder_not_less)
-  hence "b * c \<le> a * c" using nonneg by (rule mult_right_mono)
-  with this and less show False by (simp add: not_less [symmetric])
-qed  
+  using assms by (fact mult_right_less_imp_less)
 
 end