src/HOL/Rings.thy
changeset 59555 05573e5504a9
parent 59537 7f2b60cb5190
child 59557 ebd8ecacfba6
     1.1 --- a/src/HOL/Rings.thy	Wed Feb 18 22:46:47 2015 +0100
     1.2 +++ b/src/HOL/Rings.thy	Wed Feb 18 22:46:48 2015 +0100
     1.3 @@ -718,16 +718,6 @@
     1.4    apply simp
     1.5    done
     1.6  
     1.7 -lemma mult_less_imp_less_left:
     1.8 -  assumes "c * a < c * b" and "0 \<le> c"
     1.9 -  shows "a < b"
    1.10 -  using assms by (fact mult_left_less_imp_less)
    1.11 -
    1.12 -lemma mult_less_imp_less_right:
    1.13 -  assumes less: "a * c < b * c" and nonneg: "0 \<le> c"
    1.14 -  shows "a < b"
    1.15 -  using assms by (fact mult_right_less_imp_less)
    1.16 -
    1.17  end
    1.18  
    1.19  class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1