src/HOL/NthRoot.thy
 changeset 64122 74fde524799e parent 63721 492bb53c3420 child 64267 b9a1486e79be
```     1.1 --- a/src/HOL/NthRoot.thy	Sun Oct 09 16:27:01 2016 +0200
1.2 +++ b/src/HOL/NthRoot.thy	Mon Oct 10 15:45:41 2016 +0100
1.3 @@ -692,15 +692,12 @@
1.4    by (metis not_less not_less_iff_gr_or_eq numeral_less_iff real_sqrt_four
1.5        real_sqrt_le_iff semiring_norm(75) semiring_norm(78) semiring_norm(85))
1.6
1.7 -
1.8 -text \<open>Needed for the infinitely close relation over the nonstandard complex numbers.\<close>
1.9 -lemma lemma_sqrt_hcomplex_capprox:
1.10 -  "0 < u \<Longrightarrow> x < u/2 \<Longrightarrow> y < u/2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) < u"
1.11 +lemma sqrt_sum_squares_half_less:
1.12 +  "x < u/2 \<Longrightarrow> y < u/2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) < u"
1.13    apply (rule real_sqrt_sum_squares_less)
1.14     apply (auto simp add: abs_if field_simps)
1.15     apply (rule le_less_trans [where y = "x*2"])
1.16 -  using less_eq_real_def sqrt2_less_2
1.17 -    apply force
1.18 +  using less_eq_real_def sqrt2_less_2 apply force
1.19     apply assumption
1.20    apply (rule le_less_trans [where y = "y*2"])
1.21    using less_eq_real_def sqrt2_less_2 mult_le_cancel_left
```