--- a/src/HOL/Real_Vector_Spaces.thy Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Sat Aug 04 01:03:39 2018 +0200
@@ -1012,6 +1012,9 @@
lemma dist_triangle3: "dist x y \<le> dist a x + dist a y"
using dist_triangle2 [of x y a] by (simp add: dist_commute)
+lemma abs_dist_diff_le: "\<bar>dist a b - dist b c\<bar> \<le> dist a c"
+ using dist_triangle3[of b c a] dist_triangle2[of a b c] by simp
+
lemma dist_pos_lt: "x \<noteq> y \<Longrightarrow> 0 < dist x y"
by (simp add: zero_less_dist_iff)