--- a/src/HOL/NthRoot.thy Mon Feb 22 14:37:56 2016 +0000
+++ b/src/HOL/NthRoot.thy Tue Feb 23 15:47:39 2016 +0000
@@ -405,6 +405,9 @@
lemma real_sqrt_eq_iff [simp]: "(sqrt x = sqrt y) = (x = y)"
unfolding sqrt_def by (rule real_root_eq_iff [OF pos2])
+lemma real_less_lsqrt: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y\<^sup>2 \<Longrightarrow> sqrt x < y"
+ using real_sqrt_less_iff[of x "y\<^sup>2"] by simp
+
lemma real_le_lsqrt: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y\<^sup>2 \<Longrightarrow> sqrt x \<le> y"
using real_sqrt_le_iff[of x "y\<^sup>2"] by simp