diff options
author | 2006-04-28 14:59:16 +0000 | |
---|---|---|
committer | 2006-04-28 14:59:16 +0000 | |
commit | 2c4a6b4efe55a2c6ca9ca7b185723e7909e57269 (patch) | |
tree | e1542c8adb83ff297284eefc23a2703461713d9b /theories/Reals/Rtrigo_fun.v | |
parent | 514dce2dfe717e3ed2e37dce6467b56219d451c1 (diff) | |
parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) |
Merge commit 'upstream/8.0pl3+8.1alpha' into 8.0pl3+8.1alpha
Diffstat (limited to 'theories/Reals/Rtrigo_fun.v')
-rw-r--r-- | theories/Reals/Rtrigo_fun.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v index b0f29e5c..eaf2121e 100644 --- a/theories/Reals/Rtrigo_fun.v +++ b/theories/Reals/Rtrigo_fun.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rtrigo_fun.v,v 1.7.2.1 2004/07/16 19:31:15 herbelin Exp $ i*) +(*i $Id: Rtrigo_fun.v 8691 2006-04-10 09:23:37Z msozeau $ i*) Require Import Rbase. Require Import Rfunctions. @@ -61,10 +61,10 @@ intro; elim (IZN (up (/ eps - 1)) H0); intros; split with x; intros; rewrite (Rabs_Rabsolu (/ INR (S n))); cut (/ INR (S n) > 0). intro; rewrite (Rabs_pos_eq (/ INR (S n))). cut (/ eps - 1 < INR x). -intro; +intro ; generalize (Rlt_le_trans (/ eps - 1) (INR x) (INR n) H4 - (le_INR x n ((fun (n m:nat) (H:(m >= n)%nat) => H) x n H2))); + (le_INR x n H2)); clear H4; intro; unfold Rminus in H4; generalize (Rplus_lt_compat_l 1 (/ eps + -1) (INR n) H4); replace (1 + (/ eps + -1)) with (/ eps); [ clear H4; intro | ring ]. |