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 a95bc54b..89ee1745 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 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Rtrigo_alt.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) Require Import Rbase. Require Import Rfunctions. @@ -121,7 +121,7 @@ Proof. apply INR_fact_neq_0. apply INR_fact_neq_0. simpl in |- *; ring. - ring_nat. + ring. assert (H3 := cv_speed_pow_fact a); unfold Un in |- *; unfold Un_cv in H3; unfold R_dist in H3; unfold Un_cv in |- *; unfold R_dist in |- *; intros; elim (H3 eps H4); intros N H5. @@ -316,7 +316,7 @@ Proof. apply INR_fact_neq_0. apply INR_fact_neq_0. simpl in |- *; ring. - ring_nat. + ring. assert (H4 := cv_speed_pow_fact a0); unfold Un in |- *; unfold Un_cv in H4; unfold R_dist in H4; unfold Un_cv in |- *; unfold R_dist in |- *; intros; elim (H4 eps H5); intros N H6; exists N; intros. |