diff options
| -rw-r--r-- | theories/Reals/Rtrigo_fun.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v index 77fefdd7b6..e8bfe5ea55 100644 --- a/theories/Reals/Rtrigo_fun.v +++ b/theories/Reals/Rtrigo_fun.v @@ -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 ]. |