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