diff options
Diffstat (limited to 'theories/Reals/Rtrigo_alt.v')
| -rw-r--r-- | theories/Reals/Rtrigo_alt.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index 89ee1745..d82bafc6 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rtrigo_alt.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) +(*i $Id: Rtrigo_alt.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -137,7 +137,7 @@ Proof. ring. assert (X := exist_sin (Rsqr a)); elim X; intros. cut (x = sin a / a). - intro; rewrite H3 in p; unfold sin_in in p; unfold infinit_sum in p; + intro; rewrite H3 in p; unfold sin_in in p; unfold infinite_sum in p; unfold R_dist in p; unfold Un_cv in |- *; unfold R_dist in |- *; intros. cut (0 < eps / Rabs a). @@ -327,7 +327,7 @@ Proof. apply (fun m n p:nat => mult_le_compat_l p n m); apply le_n_S; assumption. assert (X := exist_cos (Rsqr a0)); elim X; intros. cut (x = cos a0). - intro; rewrite H4 in p; unfold cos_in in p; unfold infinit_sum in p; + intro; rewrite H4 in p; unfold cos_in in p; unfold infinite_sum in p; unfold R_dist in p; unfold Un_cv in |- *; unfold R_dist in |- *; intros. elim (p _ H5); intros N H6. |