src/HOL/NthRoot.thy

--- a/src/HOL/NthRoot.thy	Mon Jan 11 16:38:39 2016 +0100
+++ b/src/HOL/NthRoot.thy	Mon Jan 11 22:14:15 2016 +0000
@@ -425,6 +425,9 @@
 lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y"
   using real_sqrt_less_mono[of "x\<^sup>2" y] by simp
 
+lemma sqrt_le_D: "sqrt x \<le> y \<Longrightarrow> x \<le> y^2"
+  by (meson not_le real_less_rsqrt)
+
 lemma sqrt_even_pow2:
   assumes n: "even n"
   shows "sqrt (2 ^ n) = 2 ^ (n div 2)"