# HG changeset patch
# User nipkow
# Date 1575480504 -3600
# Node ID 095cf95d77255120efca21fa3ec3cb3799f51aae
# Parent  be2c2bfa54a0e43740a017a8d3dcd574d8234e02
moved segment lemmas where they belong

diff -r be2c2bfa54a0 -r 095cf95d7725 src/HOL/Analysis/Line_Segment.thy
--- a/src/HOL/Analysis/Line_Segment.thy	Wed Dec 04 15:36:58 2019 +0100
+++ b/src/HOL/Analysis/Line_Segment.thy	Wed Dec 04 18:28:24 2019 +0100
@@ -789,6 +789,57 @@
 
 lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval
 
+lemma closed_segment_neq_empty [simp]: "closed_segment a b \<noteq> {}"
+  by auto
+
+lemma open_segment_eq_empty [simp]: "open_segment a b = {} \<longleftrightarrow> a = b"
+proof -
+  { assume a1: "open_segment a b = {}"
+    have "{} \<noteq> {0::real<..<1}"
+      by simp
+    then have "a = b"
+      using a1 open_segment_image_interval by fastforce
+  } then show ?thesis by auto
+qed
+
+lemma open_segment_eq_empty' [simp]: "{} = open_segment a b \<longleftrightarrow> a = b"
+  using open_segment_eq_empty by blast
+
+lemmas segment_eq_empty = closed_segment_neq_empty open_segment_eq_empty
+
+lemma inj_segment:
+  fixes a :: "'a :: real_vector"
+  assumes "a \<noteq> b"
+    shows "inj_on (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) I"
+proof
+  fix x y
+  assume "(1 - x) *\<^sub>R a + x *\<^sub>R b = (1 - y) *\<^sub>R a + y *\<^sub>R b"
+  then have "x *\<^sub>R (b - a) = y *\<^sub>R (b - a)"
+    by (simp add: algebra_simps)
+  with assms show "x = y"
+    by (simp add: real_vector.scale_right_imp_eq)
+qed
+
+lemma finite_closed_segment [simp]: "finite(closed_segment a b) \<longleftrightarrow> a = b"
+  apply auto
+  apply (rule ccontr)
+  apply (simp add: segment_image_interval)
+  using infinite_Icc [OF zero_less_one] finite_imageD [OF _ inj_segment] apply blast
+  done
+
+lemma finite_open_segment [simp]: "finite(open_segment a b) \<longleftrightarrow> a = b"
+  by (auto simp: open_segment_def)
+
+lemmas finite_segment = finite_closed_segment finite_open_segment
+
+lemma closed_segment_eq_sing: "closed_segment a b = {c} \<longleftrightarrow> a = c \<and> b = c"
+  by auto
+
+lemma open_segment_eq_sing: "open_segment a b \<noteq> {c}"
+  by (metis finite_insert finite_open_segment insert_not_empty open_segment_image_interval)
+
+lemmas segment_eq_sing = closed_segment_eq_sing open_segment_eq_sing
+
 lemma open_segment_bound1:
   assumes "x \<in> open_segment a b"
   shows "norm (x - a) < norm (b - a)"
@@ -868,6 +919,172 @@
 
 lemmas convex_segment = convex_closed_segment convex_open_segment
 
+lemma subset_closed_segment:
+    "closed_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
+     a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
+  by auto (meson contra_subsetD convex_closed_segment convex_contains_segment)
+
+lemma subset_co_segment:
+    "closed_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
+     a \<in> open_segment c d \<and> b \<in> open_segment c d"
+using closed_segment_subset by blast
+
+lemma subset_open_segment:
+  fixes a :: "'a::euclidean_space"
+  shows "open_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
+         a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
+        (is "?lhs = ?rhs")
+proof (cases "a = b")
+  case True then show ?thesis by simp
+next
+  case False show ?thesis
+  proof
+    assume rhs: ?rhs
+    with \<open>a \<noteq> b\<close> have "c \<noteq> d"
+      using closed_segment_idem singleton_iff by auto
+    have "\<exists>uc. (1 - u) *\<^sub>R ((1 - ua) *\<^sub>R c + ua *\<^sub>R d) + u *\<^sub>R ((1 - ub) *\<^sub>R c + ub *\<^sub>R d) =
+               (1 - uc) *\<^sub>R c + uc *\<^sub>R d \<and> 0 < uc \<and> uc < 1"
+        if neq: "(1 - ua) *\<^sub>R c + ua *\<^sub>R d \<noteq> (1 - ub) *\<^sub>R c + ub *\<^sub>R d" "c \<noteq> d"
+           and "a = (1 - ua) *\<^sub>R c + ua *\<^sub>R d" "b = (1 - ub) *\<^sub>R c + ub *\<^sub>R d"
+           and u: "0 < u" "u < 1" and uab: "0 \<le> ua" "ua \<le> 1" "0 \<le> ub" "ub \<le> 1"
+        for u ua ub
+    proof -
+      have "ua \<noteq> ub"
+        using neq by auto
+      moreover have "(u - 1) * ua \<le> 0" using u uab
+        by (simp add: mult_nonpos_nonneg)
+      ultimately have lt: "(u - 1) * ua < u * ub" using u uab
+        by (metis antisym_conv diff_ge_0_iff_ge le_less_trans mult_eq_0_iff mult_le_0_iff not_less)
+      have "p * ua + q * ub < p+q" if p: "0 < p" and  q: "0 < q" for p q
+      proof -
+        have "\<not> p \<le> 0" "\<not> q \<le> 0"
+          using p q not_less by blast+
+        then show ?thesis
+          by (metis \<open>ua \<noteq> ub\<close> add_less_cancel_left add_less_cancel_right add_mono_thms_linordered_field(5)
+                    less_eq_real_def mult_cancel_left1 mult_less_cancel_left2 uab(2) uab(4))
+      qed
+      then have "(1 - u) * ua + u * ub < 1" using u \<open>ua \<noteq> ub\<close>
+        by (metis diff_add_cancel diff_gt_0_iff_gt)
+      with lt show ?thesis
+        by (rule_tac x="ua + u*(ub-ua)" in exI) (simp add: algebra_simps)
+    qed
+    with rhs \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close> show ?lhs
+      unfolding open_segment_image_interval closed_segment_def
+      by (fastforce simp add:)
+  next
+    assume lhs: ?lhs
+    with \<open>a \<noteq> b\<close> have "c \<noteq> d"
+      by (meson finite_open_segment rev_finite_subset)
+    have "closure (open_segment a b) \<subseteq> closure (open_segment c d)"
+      using lhs closure_mono by blast
+    then have "closed_segment a b \<subseteq> closed_segment c d"
+      by (simp add: \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close>)
+    then show ?rhs
+      by (force simp: \<open>a \<noteq> b\<close>)
+  qed
+qed
+
+lemma subset_oc_segment:
+  fixes a :: "'a::euclidean_space"
+  shows "open_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
+         a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
+apply (simp add: subset_open_segment [symmetric])
+apply (rule iffI)
+ apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment)
+apply (meson dual_order.trans segment_open_subset_closed)
+done
+
+lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment
+
+lemma dist_half_times2:
+  fixes a :: "'a :: real_normed_vector"
+  shows "dist ((1 / 2) *\<^sub>R (a + b)) x * 2 = dist (a+b) (2 *\<^sub>R x)"
+proof -
+  have "norm ((1 / 2) *\<^sub>R (a + b) - x) * 2 = norm (2 *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x))"
+    by simp
+  also have "... = norm ((a + b) - 2 *\<^sub>R x)"
+    by (simp add: real_vector.scale_right_diff_distrib)
+  finally show ?thesis
+    by (simp only: dist_norm)
+qed
+
+lemma closed_segment_as_ball:
+    "closed_segment a b = affine hull {a,b} \<inter> cball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
+proof (cases "b = a")
+  case True then show ?thesis by (auto simp: hull_inc)
+next
+  case False
+  then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
+                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
+                 (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)" for x
+  proof -
+    have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
+                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
+          ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
+                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a))"
+      unfolding eq_diff_eq [symmetric] by simp
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+                          norm ((a+b) - (2 *\<^sub>R x)) \<le> norm (b - a))"
+      by (simp add: dist_half_times2) (simp add: dist_norm)
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+            norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) \<le> norm (b - a))"
+      by auto
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+                norm ((1 - u * 2) *\<^sub>R (b - a)) \<le> norm (b - a))"
+      by (simp add: algebra_simps scaleR_2)
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+                          \<bar>1 - u * 2\<bar> * norm (b - a) \<le> norm (b - a))"
+      by simp
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> \<le> 1)"
+      by (simp add: mult_le_cancel_right2 False)
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)"
+      by auto
+    finally show ?thesis .
+  qed
+  show ?thesis
+    by (simp add: affine_hull_2 Set.set_eq_iff closed_segment_def *)
+qed
+
+lemma open_segment_as_ball:
+    "open_segment a b =
+     affine hull {a,b} \<inter> ball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
+proof (cases "b = a")
+  case True then show ?thesis by (auto simp: hull_inc)
+next
+  case False
+  then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
+                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
+                 (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)" for x
+  proof -
+    have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
+                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
+          ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
+                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a))"
+      unfolding eq_diff_eq [symmetric] by simp
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+                          norm ((a+b) - (2 *\<^sub>R x)) < norm (b - a))"
+      by (simp add: dist_half_times2) (simp add: dist_norm)
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+            norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) < norm (b - a))"
+      by auto
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+                norm ((1 - u * 2) *\<^sub>R (b - a)) < norm (b - a))"
+      by (simp add: algebra_simps scaleR_2)
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+                          \<bar>1 - u * 2\<bar> * norm (b - a) < norm (b - a))"
+      by simp
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> < 1)"
+      by (simp add: mult_le_cancel_right2 False)
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)"
+      by auto
+    finally show ?thesis .
+  qed
+  show ?thesis
+    using False by (force simp: affine_hull_2 Set.set_eq_iff open_segment_image_interval *)
+qed
+
+lemmas segment_as_ball = closed_segment_as_ball open_segment_as_ball
+
 lemma connected_segment [iff]:
   fixes x :: "'a :: real_normed_vector"
   shows "connected (closed_segment x y)"
diff -r be2c2bfa54a0 -r 095cf95d7725 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Wed Dec 04 15:36:58 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Wed Dec 04 18:28:24 2019 +0100
@@ -79,226 +79,6 @@
     by (meson hull_mono inf_mono subset_insertI subset_refl)
 qed
 
-subsection\<^marker>\<open>tag unimportant\<close>\<open>More results about segments\<close>
-
-lemma dist_half_times2:
-  fixes a :: "'a :: real_normed_vector"
-  shows "dist ((1 / 2) *\<^sub>R (a + b)) x * 2 = dist (a+b) (2 *\<^sub>R x)"
-proof -
-  have "norm ((1 / 2) *\<^sub>R (a + b) - x) * 2 = norm (2 *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x))"
-    by simp
-  also have "... = norm ((a + b) - 2 *\<^sub>R x)"
-    by (simp add: real_vector.scale_right_diff_distrib)
-  finally show ?thesis
-    by (simp only: dist_norm)
-qed
-
-lemma closed_segment_as_ball:
-    "closed_segment a b = affine hull {a,b} \<inter> cball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
-proof (cases "b = a")
-  case True then show ?thesis by (auto simp: hull_inc)
-next
-  case False
-  then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
-                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
-                 (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)" for x
-  proof -
-    have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
-                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
-          ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
-                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a))"
-      unfolding eq_diff_eq [symmetric] by simp
-    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
-                          norm ((a+b) - (2 *\<^sub>R x)) \<le> norm (b - a))"
-      by (simp add: dist_half_times2) (simp add: dist_norm)
-    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
-            norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) \<le> norm (b - a))"
-      by auto
-    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
-                norm ((1 - u * 2) *\<^sub>R (b - a)) \<le> norm (b - a))"
-      by (simp add: algebra_simps scaleR_2)
-    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
-                          \<bar>1 - u * 2\<bar> * norm (b - a) \<le> norm (b - a))"
-      by simp
-    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> \<le> 1)"
-      by (simp add: mult_le_cancel_right2 False)
-    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)"
-      by auto
-    finally show ?thesis .
-  qed
-  show ?thesis
-    by (simp add: affine_hull_2 Set.set_eq_iff closed_segment_def *)
-qed
-
-lemma open_segment_as_ball:
-    "open_segment a b =
-     affine hull {a,b} \<inter> ball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
-proof (cases "b = a")
-  case True then show ?thesis by (auto simp: hull_inc)
-next
-  case False
-  then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
-                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
-                 (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)" for x
-  proof -
-    have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
-                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
-          ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
-                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a))"
-      unfolding eq_diff_eq [symmetric] by simp
-    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
-                          norm ((a+b) - (2 *\<^sub>R x)) < norm (b - a))"
-      by (simp add: dist_half_times2) (simp add: dist_norm)
-    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
-            norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) < norm (b - a))"
-      by auto
-    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
-                norm ((1 - u * 2) *\<^sub>R (b - a)) < norm (b - a))"
-      by (simp add: algebra_simps scaleR_2)
-    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
-                          \<bar>1 - u * 2\<bar> * norm (b - a) < norm (b - a))"
-      by simp
-    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> < 1)"
-      by (simp add: mult_le_cancel_right2 False)
-    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)"
-      by auto
-    finally show ?thesis .
-  qed
-  show ?thesis
-    using False by (force simp: affine_hull_2 Set.set_eq_iff open_segment_image_interval *)
-qed
-
-lemmas segment_as_ball = closed_segment_as_ball open_segment_as_ball
-
-lemma closed_segment_neq_empty [simp]: "closed_segment a b \<noteq> {}"
-  by auto
-
-lemma open_segment_eq_empty [simp]: "open_segment a b = {} \<longleftrightarrow> a = b"
-proof -
-  { assume a1: "open_segment a b = {}"
-    have "{} \<noteq> {0::real<..<1}"
-      by simp
-    then have "a = b"
-      using a1 open_segment_image_interval by fastforce
-  } then show ?thesis by auto
-qed
-
-lemma open_segment_eq_empty' [simp]: "{} = open_segment a b \<longleftrightarrow> a = b"
-  using open_segment_eq_empty by blast
-
-lemmas segment_eq_empty = closed_segment_neq_empty open_segment_eq_empty
-
-lemma inj_segment:
-  fixes a :: "'a :: real_vector"
-  assumes "a \<noteq> b"
-    shows "inj_on (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) I"
-proof
-  fix x y
-  assume "(1 - x) *\<^sub>R a + x *\<^sub>R b = (1 - y) *\<^sub>R a + y *\<^sub>R b"
-  then have "x *\<^sub>R (b - a) = y *\<^sub>R (b - a)"
-    by (simp add: algebra_simps)
-  with assms show "x = y"
-    by (simp add: real_vector.scale_right_imp_eq)
-qed
-
-lemma finite_closed_segment [simp]: "finite(closed_segment a b) \<longleftrightarrow> a = b"
-  apply auto
-  apply (rule ccontr)
-  apply (simp add: segment_image_interval)
-  using infinite_Icc [OF zero_less_one] finite_imageD [OF _ inj_segment] apply blast
-  done
-
-lemma finite_open_segment [simp]: "finite(open_segment a b) \<longleftrightarrow> a = b"
-  by (auto simp: open_segment_def)
-
-lemmas finite_segment = finite_closed_segment finite_open_segment
-
-lemma closed_segment_eq_sing: "closed_segment a b = {c} \<longleftrightarrow> a = c \<and> b = c"
-  by auto
-
-lemma open_segment_eq_sing: "open_segment a b \<noteq> {c}"
-  by (metis finite_insert finite_open_segment insert_not_empty open_segment_image_interval)
-
-lemmas segment_eq_sing = closed_segment_eq_sing open_segment_eq_sing
-
-lemma subset_closed_segment:
-    "closed_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
-     a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
-  by auto (meson contra_subsetD convex_closed_segment convex_contains_segment)
-
-lemma subset_co_segment:
-    "closed_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
-     a \<in> open_segment c d \<and> b \<in> open_segment c d"
-using closed_segment_subset by blast
-
-lemma subset_open_segment:
-  fixes a :: "'a::euclidean_space"
-  shows "open_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
-         a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
-        (is "?lhs = ?rhs")
-proof (cases "a = b")
-  case True then show ?thesis by simp
-next
-  case False show ?thesis
-  proof
-    assume rhs: ?rhs
-    with \<open>a \<noteq> b\<close> have "c \<noteq> d"
-      using closed_segment_idem singleton_iff by auto
-    have "\<exists>uc. (1 - u) *\<^sub>R ((1 - ua) *\<^sub>R c + ua *\<^sub>R d) + u *\<^sub>R ((1 - ub) *\<^sub>R c + ub *\<^sub>R d) =
-               (1 - uc) *\<^sub>R c + uc *\<^sub>R d \<and> 0 < uc \<and> uc < 1"
-        if neq: "(1 - ua) *\<^sub>R c + ua *\<^sub>R d \<noteq> (1 - ub) *\<^sub>R c + ub *\<^sub>R d" "c \<noteq> d"
-           and "a = (1 - ua) *\<^sub>R c + ua *\<^sub>R d" "b = (1 - ub) *\<^sub>R c + ub *\<^sub>R d"
-           and u: "0 < u" "u < 1" and uab: "0 \<le> ua" "ua \<le> 1" "0 \<le> ub" "ub \<le> 1"
-        for u ua ub
-    proof -
-      have "ua \<noteq> ub"
-        using neq by auto
-      moreover have "(u - 1) * ua \<le> 0" using u uab
-        by (simp add: mult_nonpos_nonneg)
-      ultimately have lt: "(u - 1) * ua < u * ub" using u uab
-        by (metis antisym_conv diff_ge_0_iff_ge le_less_trans mult_eq_0_iff mult_le_0_iff not_less)
-      have "p * ua + q * ub < p+q" if p: "0 < p" and  q: "0 < q" for p q
-      proof -
-        have "\<not> p \<le> 0" "\<not> q \<le> 0"
-          using p q not_less by blast+
-        then show ?thesis
-          by (metis \<open>ua \<noteq> ub\<close> add_less_cancel_left add_less_cancel_right add_mono_thms_linordered_field(5)
-                    less_eq_real_def mult_cancel_left1 mult_less_cancel_left2 uab(2) uab(4))
-      qed
-      then have "(1 - u) * ua + u * ub < 1" using u \<open>ua \<noteq> ub\<close>
-        by (metis diff_add_cancel diff_gt_0_iff_gt)
-      with lt show ?thesis
-        by (rule_tac x="ua + u*(ub-ua)" in exI) (simp add: algebra_simps)
-    qed
-    with rhs \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close> show ?lhs
-      unfolding open_segment_image_interval closed_segment_def
-      by (fastforce simp add:)
-  next
-    assume lhs: ?lhs
-    with \<open>a \<noteq> b\<close> have "c \<noteq> d"
-      by (meson finite_open_segment rev_finite_subset)
-    have "closure (open_segment a b) \<subseteq> closure (open_segment c d)"
-      using lhs closure_mono by blast
-    then have "closed_segment a b \<subseteq> closed_segment c d"
-      by (simp add: \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close>)
-    then show ?rhs
-      by (force simp: \<open>a \<noteq> b\<close>)
-  qed
-qed
-
-lemma subset_oc_segment:
-  fixes a :: "'a::euclidean_space"
-  shows "open_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
-         a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
-apply (simp add: subset_open_segment [symmetric])
-apply (rule iffI)
- apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment)
-apply (meson dual_order.trans segment_open_subset_closed)
-done
-
-lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment
-
-
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Shrinking towards the interior of a convex set\<close>
 
 lemma mem_interior_convex_shrink: