src/HOL/Multivariate_Analysis/Linear_Algebra.thy

   have "y^2 + z^2 \<le> y^2 + 2*y*z + z^2" using z y by (simp add: mult_nonneg_nonneg)
   with xy have th: "x ^2 \<le> (y+z)^2" by (simp add: power2_eq_square field_simps)
   from y z have yz: "y + z \<ge> 0" by arith
   from power2_le_imp_le[OF th yz] show ?thesis .
 qed
-
-text {* TODO: move to NthRoot *}
-lemma sqrt_add_le_add_sqrt:
-  assumes x: "0 \<le> x" and y: "0 \<le> y"
-  shows "sqrt (x + y) \<le> sqrt x + sqrt y"
-apply (rule power2_le_imp_le)
-apply (simp add: power2_sum x y)
-apply (simp add: mult_nonneg_nonneg x y)
-apply (simp add: x y)
-done
 
 subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *}
 
 definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "hull" 75) where
   "S hull s = Inter {t. S t \<and> s \<subseteq> t}"