src/HOL/Real_Vector_Spaces.thy

--- a/src/HOL/Real_Vector_Spaces.thy	Wed Feb 17 21:51:56 2016 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -9,9 +9,6 @@
 imports Real Topological_Spaces
 begin
 
-lemma (in ordered_ab_group_add) diff_ge_0_iff_ge [simp]: "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
-  by (simp add: le_diff_eq)
-
 subsection \<open>Locale for additive functions\<close>
 
 locale additive =