diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-10 09:23:37 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-10 09:23:37 +0000 |
| commit | 79fa2898ba31a2bfa484f3e9ac693ff714365758 (patch) | |
| tree | bf2444537889ae7226a0093ada637cd9a1cab6e4 /theories/Reals/Rtrigo_fun.v | |
| parent | ef316e533fdd5f3ea599c958551707c9d75aab97 (diff) | |
New unification can solve the problem without eta-expansion,
but is bugguy with it. Temporary fix.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8691 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo_fun.v')
| -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 77fefdd7b..e8bfe5ea5 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 ]. |