src/HOL/Multivariate_Analysis/Linear_Algebra.thy

 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: real_sum_squared_expand x y)
+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). *}