src/HOL/Rings.thy
changeset 59000 6eb0725503fc
parent 58952 5d82cdef6c1b
child 59009 348561aa3869
     1.1 --- a/src/HOL/Rings.thy	Thu Nov 13 14:40:06 2014 +0100
     1.2 +++ b/src/HOL/Rings.thy	Thu Nov 13 17:19:52 2014 +0100
     1.3 @@ -1021,6 +1021,12 @@
     1.4    using assms mult_strict_mono [of 1 m 1 n]
     1.5      by (simp add:  less_trans [OF zero_less_one]) 
     1.6  
     1.7 +lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"
     1.8 +  using mult_left_mono[of c 1 a] by simp
     1.9 +
    1.10 +lemma mult_le_one: "a \<le> 1 \<Longrightarrow> 0 \<le> b \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b \<le> 1"
    1.11 +  using mult_mono[of a 1 b 1] by simp
    1.12 +
    1.13  end
    1.14  
    1.15  class linordered_idom = comm_ring_1 +