# HG changeset patch
# User huffman
# Date 1176256493 -7200
# Node ID 2a9b64b26612ee12f48e2139ef06b4def700533a
# Parent  73771f4548611f92902d6e1ed6c34797ba609676
move lemma real_of_nat_inverse_le_iff from NSA.thy to NthRoot.thy

diff -r 73771f454861 -r 2a9b64b26612 src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Wed Apr 11 02:19:06 2007 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Wed Apr 11 03:54:53 2007 +0200
@@ -2188,15 +2188,6 @@
 apply (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le)
 done
 
-lemma real_of_nat_inverse_le_iff:
-     "(inverse (real(Suc n)) \<le> r) = (1 \<le> r * real(Suc n))"
-apply (simp (no_asm) add: linorder_not_less [symmetric])
-apply (simp (no_asm) add: inverse_eq_divide)
-apply (subst pos_less_divide_eq)
-apply (simp (no_asm) add: real_of_nat_Suc_gt_zero)
-apply (simp (no_asm) add: real_mult_commute)
-done
-
 lemma real_of_nat_inverse_eq_iff:
      "(u = inverse (real(Suc n))) = (real(Suc n) = inverse u)"
 by (auto simp add: real_of_nat_Suc_gt_zero real_not_refl2 [THEN not_sym])
diff -r 73771f454861 -r 2a9b64b26612 src/HOL/Hyperreal/NthRoot.thy
--- a/src/HOL/Hyperreal/NthRoot.thy	Wed Apr 11 02:19:06 2007 +0200
+++ b/src/HOL/Hyperreal/NthRoot.thy	Wed Apr 11 03:54:53 2007 +0200
@@ -128,6 +128,10 @@
             simp add: add_assoc [symmetric] neg_less_0_iff_less)
 done
 
+lemma real_of_nat_inverse_le_iff:
+  "(inverse (real(Suc n)) \<le> r) = (1 \<le> r * real(Suc n))"
+by (simp add: inverse_eq_divide pos_divide_le_eq)
+
 lemma real_mult_add_one_minus_ge_zero:
      "0 < r ==>  0 <= r*(1 + -inverse(real (Suc n)))"
 by (simp add: zero_le_mult_iff real_of_nat_inverse_le_iff real_0_le_add_iff)