diff -r df57e4e3c0b7 -r 8f85bb443d33 src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Mon Oct 26 23:42:01 2015 +0000
+++ b/src/HOL/Library/Convex.thy	Tue Oct 27 15:17:02 2015 +0000
@@ -48,6 +48,14 @@
   shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \<in> s"
   using assms unfolding convex_alt by auto
 
+lemma mem_convex_alt:
+  assumes "convex S" "x \<in> S" "y \<in> S" "u \<ge> 0" "v \<ge> 0" "u + v > 0"
+  shows "((u/(u+v)) *\<^sub>R x + (v/(u+v)) *\<^sub>R y) \<in> S"
+  apply (rule convexD)
+  using assms
+  apply (simp_all add: zero_le_divide_iff add_divide_distrib [symmetric])
+  done
+
 lemma convex_empty[intro,simp]: "convex {}"
   unfolding convex_def by simp