--- a/src/HOL/Analysis/Linear_Algebra.thy Sun Nov 07 20:04:47 2021 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy Sun Nov 07 22:14:40 2021 +0000
@@ -1143,6 +1143,15 @@
finally show ?thesis .
qed
+lemma dist_triangle_eq:
+ fixes x y z :: "'a::real_inner"
+ shows "dist x z = dist x y + dist y z \<longleftrightarrow>
+ norm (x - y) *\<^sub>R (y - z) = norm (y - z) *\<^sub>R (x - y)"
+proof -
+ have *: "x - y + (y - z) = x - z" by auto
+ show ?thesis unfolding dist_norm norm_triangle_eq[of "x - y" "y - z", unfolded *]
+ by (auto simp:norm_minus_commute)
+qed
subsection \<open>Collinearity\<close>