src/HOL/Real_Vector_Spaces.thy

--- a/src/HOL/Real_Vector_Spaces.thy	Sun Aug 13 23:45:45 2017 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Aug 14 18:54:25 2017 +0100
@@ -825,6 +825,9 @@
   then show ?thesis by simp
 qed
 
+lemma norm_triangle_le_diff: "norm x + norm y \<le> e \<Longrightarrow> norm (x - y) \<le> e"
+  by (meson norm_triangle_ineq4 order_trans)
+
 lemma norm_diff_ineq: "norm a - norm b \<le> norm (a + b)"
   for a b :: "'a::real_normed_vector"
 proof -