src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy

     apply rule
     apply (rule ccontr)
     using \<open>y \<in> s\<close>
   proof -
     show "inner (y - z) z < inner (y - z) y"
-      apply (subst diff_less_iff(1)[symmetric])
+      apply (subst diff_gt_0_iff_gt [symmetric])
       unfolding inner_diff_right[symmetric] and inner_gt_zero_iff
       using \<open>y\<in>s\<close> \<open>z\<notin>s\<close>
       apply auto
       done
   next