src/HOL/Hyperreal/NthRoot.thy
changeset 22630 2a9b64b26612
parent 22443 346729a55460
child 22721 d9be18bd7a28
     1.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Wed Apr 11 02:19:06 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Wed Apr 11 03:54:53 2007 +0200
     1.3 @@ -128,6 +128,10 @@
     1.4              simp add: add_assoc [symmetric] neg_less_0_iff_less)
     1.5  done
     1.6  
     1.7 +lemma real_of_nat_inverse_le_iff:
     1.8 +  "(inverse (real(Suc n)) \<le> r) = (1 \<le> r * real(Suc n))"
     1.9 +by (simp add: inverse_eq_divide pos_divide_le_eq)
    1.10 +
    1.11  lemma real_mult_add_one_minus_ge_zero:
    1.12       "0 < r ==>  0 <= r*(1 + -inverse(real (Suc n)))"
    1.13  by (simp add: zero_le_mult_iff real_of_nat_inverse_le_iff real_0_le_add_iff)