diff -r 00c436488398 -r bdff8bf0a75b src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/NthRoot.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -480,6 +480,9 @@
 lemma sqrt_le_D: "sqrt x \<le> y \<Longrightarrow> x \<le> y\<^sup>2"
   by (meson not_le real_less_rsqrt)
 
+lemma sqrt_ge_absD: "\<bar>x\<bar> \<le> sqrt y \<Longrightarrow> x\<^sup>2 \<le> y"
+  using real_sqrt_le_iff[of "x\<^sup>2"] by simp
+
 lemma sqrt_even_pow2:
   assumes n: "even n"
   shows "sqrt (2 ^ n) = 2 ^ (n div 2)"
@@ -538,6 +541,8 @@
   DERIV_real_sqrt_generic[THEN DERIV_chain2, derivative_intros]
   DERIV_real_root_generic[THEN DERIV_chain2, derivative_intros]
 
+lemmas has_derivative_real_sqrt[derivative_intros] = DERIV_real_sqrt[THEN DERIV_compose_FDERIV]
+
 lemma not_real_square_gt_zero [simp]: "\<not> 0 < x * x \<longleftrightarrow> x = 0"
   for x :: real
   apply auto
@@ -658,6 +663,13 @@
 lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)"
   by (simp add: power2_eq_square [symmetric])
 
+lemma sqrt_sum_squares_le_sum:
+  "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) \<le> x + y"
+  apply (rule power2_le_imp_le)
+  apply (simp add: power2_sum)
+  apply simp
+  done
+
 lemma real_sqrt_sum_squares_triangle_ineq:
   "sqrt ((a + c)\<^sup>2 + (b + d)\<^sup>2) \<le> sqrt (a\<^sup>2 + b\<^sup>2) + sqrt (c\<^sup>2 + d\<^sup>2)"
   apply (rule power2_le_imp_le)