# HG changeset patch
# User huffman
# Date 1180463502 -7200
# Node ID 3d853d6f2f7d2edc6891a4faad346e4f5215c068
# Parent  5feeb93b3ba8ccb38ea6c6cf0ecf05d4025d397f
add lemma real_sqrt_sum_squares_less

diff -r 5feeb93b3ba8 -r 3d853d6f2f7d src/HOL/Hyperreal/NthRoot.thy
--- a/src/HOL/Hyperreal/NthRoot.thy	Tue May 29 18:31:30 2007 +0200
+++ b/src/HOL/Hyperreal/NthRoot.thy	Tue May 29 20:31:42 2007 +0200
@@ -536,6 +536,16 @@
 apply (simp add: add_increasing)
 done
 
+lemma real_sqrt_sum_squares_less:
+  "\<lbrakk>\<bar>x\<bar> < u / sqrt 2; \<bar>y\<bar> < u / sqrt 2\<rbrakk> \<Longrightarrow> sqrt (x\<twosuperior> + y\<twosuperior>) < u"
+apply (rule power2_less_imp_less, simp)
+apply (drule power_strict_mono [OF _ abs_ge_zero pos2])
+apply (drule power_strict_mono [OF _ abs_ge_zero pos2])
+apply (simp add: power_divide)
+apply (drule order_le_less_trans [OF abs_ge_zero])
+apply (simp add: zero_less_divide_iff)
+done
+
 text{*Needed for the infinitely close relation over the nonstandard
     complex numbers*}
 lemma lemma_sqrt_hcomplex_capprox: