src/HOL/Real_Vector_Spaces.thy
changeset 60303 00c06f1315d0
parent 60155 91477b3a2d6b
child 60307 75e1aa7a450e
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Mon May 25 22:52:17 2015 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue May 26 21:58:04 2015 +0100
     1.3 @@ -518,6 +518,13 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma neg_le_divideR_eq:
     1.8 +  fixes a :: "'a :: ordered_real_vector"
     1.9 +  assumes "c < 0"
    1.10 +  shows "a \<le> b /\<^sub>R c \<longleftrightarrow> b \<le> c *\<^sub>R a"
    1.11 +  using pos_le_divideR_eq [of "-c" a "-b"] assms
    1.12 +  by simp
    1.13 +
    1.14  lemma scaleR_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> (x::'a::ordered_real_vector) \<Longrightarrow> 0 \<le> a *\<^sub>R x"
    1.15    using scaleR_left_mono [of 0 x a]
    1.16    by simp