explicit instance real::ordered_real_vector before subclass in ordered_euclidean_space

--- a/src/HOL/Real_Vector_Spaces.thy	Tue Aug 27 19:22:57 2019 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Tue Aug 27 22:31:21 2019 +0200
@@ -1213,6 +1213,9 @@
 lemmas closed_real_atLeast = closed_atLeast[where 'a=real]
 lemmas closed_real_atLeastAtMost = closed_atLeastAtMost[where 'a=real]
 
+instance real :: ordered_real_vector
+  by standard (auto intro: mult_left_mono mult_right_mono)
+
 
 subsection \<open>Extra type constraints\<close>