Imported Upstream version 8.1+dfsgupstream/8.1+dfsg

16 files changed, 87 insertions, 68 deletions

diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index fa44b6ff..581c181f 100644
--- a/theories/Reals/AltSeries.v
+++ b/theories/Reals/AltSeries.v
@@ -6,7 +6,7 @@
   (*         *       GNU Lesser General Public License Version 2.1        *)
   (************************************************************************)
 
-  (*i $Id: AltSeries.v 9245 2006-10-17 12:53:34Z notin $ i*)
+  (*i $Id: AltSeries.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -92,9 +92,9 @@ Proof.
     replace (Un (S (2 * S N)) + (-1 * Un (S (2 * S N)) + Un (S (S (2 * S N)))))
       with (Un (S (S (2 * S N)))); [ idtac | ring ].
   apply H.
-  ring_nat.
+  ring.
   apply HrecN.
-  ring_nat.
+  ring.
 Qed.
 
 (** A more general inequality *)
@@ -300,7 +300,7 @@ Proof.
   do 2 rewrite Rmult_1_r; apply le_INR.
   replace (2 * S n + 1)%nat with (S (S (2 * n + 1))).
   apply le_trans with (S (2 * n + 1)); apply le_n_Sn.
-  ring_nat.
+  ring.
   apply not_O_INR; discriminate.
   apply not_O_INR; replace (2 * n + 1)%nat with (S (2 * n));
     [ discriminate | ring ].
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index 48876be2..7dbbd605 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -6,7 +6,7 @@
   (*         *       GNU Lesser General Public License Version 2.1        *)
   (************************************************************************)
 
-  (*i $Id: ArithProp.v 9245 2006-10-17 12:53:34Z notin $ i*)
+  (*i $Id: ArithProp.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rbasic_fun.
@@ -75,7 +75,7 @@ Proof.
   apply H3; assumption.
   right.
   apply H4; assumption.
-  unfold double in |- *; ring.
+  unfold double in |- *;ring.
 Qed.
 
   (* 2m <= 2n => m<=n *)
diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index 3719d551..10965951 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -6,7 +6,7 @@
   (*         *       GNU Lesser General Public License Version 2.1        *)
   (************************************************************************)
 
-  (*i $Id: Cos_plus.v 9245 2006-10-17 12:53:34Z notin $ i*)
+  (*i $Id: Cos_plus.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -486,7 +486,7 @@ Proof.
   apply le_trans with (pred N).
   assumption.
   apply le_pred_n.
-  ring_nat.
+  ring.
   apply Rle_trans with
     (sum_f_R0
       (fun k:nat =>
@@ -515,7 +515,7 @@ Proof.
   apply le_trans with (2 * S (S (n0 + n)))%nat.
   replace (2 * S (S (n0 + n)))%nat with (S (2 * S (n0 + n) + 1)).
   apply le_n_Sn.
-  ring_nat.
+  ring.
   omega.
   right.
   unfold Rdiv in |- *; rewrite Rmult_comm.
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index ac8ffbeb..d410e14a 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
  
-(*i $Id: Cos_rel.v 9178 2006-09-26 11:18:22Z barras $ i*)
+(*i $Id: Cos_rel.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -109,9 +109,10 @@ pose
              C (2 * S p) (S (2 * l)) * x ^ S (2 * l) * y ^ S (2 * (p - l))) p
     end).
 ring_simplify.
+unfold Rminus.
 replace
 (* (-   old ring compat *)
- (-1 *
+ (-
   sum_f_R0
     (fun k:nat =>
        sum_f_R0
@@ -140,7 +141,6 @@ replace
     (fun l:nat =>
        C (2 * S i) (S (2 * l)) * x ^ S (2 * l) * y ^ S (2 * (i - l))) i) with
  (sum_f_R0 (fun l:nat => Wn (S (2 * l))) i).
-(*rewrite Rplus_comm.*) (* compatibility old ring... *)
 apply sum_decomposition.
 apply sum_eq; intros.
 unfold Wn in |- *.
@@ -154,8 +154,7 @@ apply Rmult_eq_compat_l.
 replace (2 * S i - 2 * i0)%nat with (2 * (S i - i0))%nat.
 reflexivity.
 omega.
-replace (sum_f_R0 sin_nnn (S n)) with (-1 * (-1 * sum_f_R0 sin_nnn (S n))).
-(*replace (* compatibility old ring... *)
+replace
  (-
   sum_f_R0
     (fun k:nat =>
@@ -171,13 +170,13 @@ replace (sum_f_R0 sin_nnn (S n)) with (-1 * (-1 * sum_f_R0 sin_nnn (S n))).
          (fun p:nat =>
             (-1) ^ p / INR (fact (2 * p + 1)) * x ^ (2 * p + 1) *
             ((-1) ^ (k - p) / INR (fact (2 * (k - p) + 1)) *
-             y ^ (2 * (k - p) + 1))) k) n);[idtac|ring].*)
-apply Rmult_eq_compat_l.
+             y ^ (2 * (k - p) + 1))) k) n);[idtac|ring].
 rewrite scal_sum.
 rewrite decomp_sum.
 replace (sin_nnn 0%nat) with 0.
-rewrite Rmult_0_l; rewrite Rplus_0_l.
-replace (pred (S n)) with n; [ idtac | reflexivity ].
+rewrite Rplus_0_l.
+change (pred (S n)) with n.
+   (* replace (pred (S n)) with n; [ idtac | reflexivity ]. *)
 apply sum_eq; intros.
 rewrite Rmult_comm.
 unfold sin_nnn in |- *.
@@ -185,8 +184,8 @@ rewrite scal_sum.
 rewrite scal_sum.
 apply sum_eq; intros.
 unfold Rdiv in |- *.
-repeat rewrite Rmult_assoc.
-rewrite (Rmult_comm (/ INR (fact (2 * S i)))).
+(*repeat rewrite Rmult_assoc.*)
+(* rewrite (Rmult_comm (/ INR (fact (2 * S i)))). *)
 repeat rewrite <- Rmult_assoc.
 rewrite <- (Rmult_comm (/ INR (fact (2 * S i)))).
 repeat rewrite <- Rmult_assoc.
@@ -216,7 +215,7 @@ apply INR_fact_neq_0.
 apply INR_fact_neq_0.
 reflexivity.
 apply lt_O_Sn.
-ring.
+(* ring. *)
 apply sum_eq; intros.
 rewrite scal_sum.
 apply sum_eq; intros.
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index 5dafec83..beb4b744 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Exp_prop.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Exp_prop.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -87,7 +87,7 @@ Proof.
   reflexivity.
   replace (2 * S N)%nat with (S (S (2 * N))).
   simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma div2_S_double : forall N:nat, div2 (S (2 * N)) = N.
@@ -96,7 +96,7 @@ Proof.
   reflexivity.
   replace (2 * S N)%nat with (S (S (2 * N))).
   simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma div2_not_R0 : forall N:nat, (1 < N)%nat -> (0 < div2 N)%nat.
@@ -367,7 +367,7 @@ Proof.
   apply le_trans with (pred N).
   apply H0.
   apply le_pred_n.
-  rewrite H4; ring_nat.
+  rewrite H4; ring.
   cut (S N = (2 * S N0)%nat).
   intro.
   replace (C (S N) (S N0) / INR (fact (S N))) with (/ Rsqr (INR (fact (S N0)))).
@@ -388,7 +388,7 @@ Proof.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
-  rewrite H4; ring_nat.
+  rewrite H4; ring.
   unfold C, Rdiv in |- *.
   rewrite (Rmult_comm (INR (fact (S N)))).
   rewrite Rmult_assoc; rewrite <- Rinv_r_sym.
@@ -494,7 +494,7 @@ Proof.
   simpl in |- *.
   pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
     apply Rlt_0_1.
-  ring_nat.
+  ring.
   unfold Rsqr in |- *; apply prod_neq_R0; apply INR_fact_neq_0.
   unfold Rsqr in |- *; apply prod_neq_R0; apply not_O_INR; discriminate.
   assert (H0 := even_odd_cor N).
@@ -515,7 +515,7 @@ Proof.
   replace (S (S (2 * N0))) with (2 * S N0)%nat.
   do 2 rewrite div2_double.
   reflexivity.
-  ring_nat.
+  ring.
   apply S_pred with 0%nat; apply H.
 Qed.
 
@@ -585,8 +585,8 @@ Proof.
   apply (fun m n p:nat => mult_le_compat_l p n m).
   replace (2 * S N1)%nat with (S (S (2 * N1))).
   apply le_n_Sn.
-  ring_nat.
-  ring_nat.
+  ring.
+  ring.
   reflexivity.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
@@ -623,7 +623,7 @@ Proof.
   replace (2 * N1)%nat with (S (S (2 * pred N1))).
   reflexivity.
   pattern N1 at 2 in |- *; replace N1 with (S (pred N1)).
-  ring_nat.
+  ring.
   symmetry  in |- *; apply S_pred with 0%nat; apply H8.
   apply INR_lt.
   apply Rmult_lt_reg_l with (INR 2).
@@ -641,7 +641,7 @@ Proof.
   rewrite div2_double.
   replace (2 * S N1)%nat with (S (S (2 * N1))).
   apply le_n_Sn.
-  ring_nat.
+  ring.
   reflexivity.
   apply le_trans with (max (2 * S N0) 2).
   apply le_max_l.
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index 11c6378e..a8f72302 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: PartSum.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: PartSum.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -278,7 +278,7 @@ Proof.
   rewrite (tech5 An (2 * S N)).
   rewrite <- HrecN.
   ring.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma sum_Rle :
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 51c66afa..7d98a844 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -6,13 +6,15 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: RIneq.v 9302 2006-10-27 21:21:17Z barras $ i*)
+(*i $Id: RIneq.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 (***************************************************************************)
 (**              Basic lemmas for the classical reals numbers              *)
 (***************************************************************************)
 
 Require Export Raxioms.
+Require Import Rpow_def.
+Require Import Zpower.
 Require Export ZArithRing.
 Require Import Omega.
 Require Export RealField.
@@ -1528,6 +1530,16 @@ Proof.
   rewrite Rmult_opp_opp; auto with real.
 Qed.
 
+Lemma pow_IZR : forall z n, pow (IZR z) n = IZR (Zpower z (Z_of_nat n)).
+Proof.
+ intros z [|n];simpl;trivial.
+ rewrite Zpower_pos_nat.
+ rewrite nat_of_P_o_P_of_succ_nat_eq_succ. unfold Zpower_nat;simpl.
+ rewrite mult_IZR.
+ induction n;simpl;trivial.
+ rewrite mult_IZR;ring[IHn].
+Qed.
+
 (**********)
 Lemma Ropp_Ropp_IZR : forall n:Z, IZR (- n) = - IZR n.
 Proof.
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index f9ba589e..330c0042 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*i $Id: Rdefinitions.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rdefinitions.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 
 (*********************************************************)
@@ -55,6 +55,8 @@ Definition Rminus (r1 r2:R) : R := (r1 + - r2)%R.
 (**********)
 Definition Rdiv (r1 r2:R) : R := (r1 * / r2)%R.
 
+(**********)
+
 Infix "-" := Rminus : R_scope.
 Infix "/" := Rdiv : R_scope.
 
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index c727623c..3d1c0375 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rfunctions.v 9302 2006-10-27 21:21:17Z barras $ i*)
+(*i $Id: Rfunctions.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 (*i Some properties about pow and sum have been made with John Harrison i*)
 (*i Some Lemmas (about pow and powerRZ) have been done by Laurent Thery i*)
@@ -15,10 +15,10 @@
 (**          Definition of the sum functions            *)
 (*                                                      *)
 (********************************************************)
-Require Export LegacyArithRing. (* for ring_nat... *)
 Require Export ArithRing.
 
 Require Import Rbase.
+Require Export Rpow_def.
 Require Export R_Ifp.
 Require Export Rbasic_fun.
 Require Export R_sqr.
@@ -65,11 +65,6 @@ Qed.
 (** *       Power              *)
 (*******************************)
 (*********)
-Boxed Fixpoint pow (r:R) (n:nat) {struct n} : R :=
-  match n with
-    | O => 1
-    | S n => r * pow r n
-  end.
 
 Infix "^" := pow : R_scope.
 
@@ -382,7 +377,7 @@ Proof.
   replace (x ^ S (S (2 * n))) with (x * x * x ^ (2 * n)).
   rewrite Hrecn; reflexivity.
   simpl in |- *; ring.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma pow_le : forall (a:R) (n:nat), 0 <= a -> 0 <= a ^ n.
@@ -429,7 +424,7 @@ Proof.
   rewrite Hrecn2.
   simpl in |- *.
   ring.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma pow_incr : forall (x y:R) (n:nat), 0 <= x <= y -> x ^ n <= y ^ n.
diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v
new file mode 100644
index 00000000..5bdbb76b
--- /dev/null
+++ b/theories/Reals/Rpow_def.v
@@ -0,0 +1,7 @@
+Require Import Rdefinitions.
+
+Fixpoint pow (r:R) (n:nat) {struct n} : R :=
+  match n with
+    | O => R1
+    | S n => Rmult r (pow r n)
+  end.
diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
index 690c420f..cb31d3b2 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rsigma.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rsigma.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -53,7 +53,7 @@ Section Sigma.
     apply lt_minus_O_lt; assumption.
     apply sum_eq; intros; replace (S k + S i)%nat with (S (S k) + i)%nat.
     reflexivity.
-    ring_nat.
+    ring.
     replace (high - S (S k))%nat with (high - S k - 1)%nat.
     apply pred_of_minus.
     omega.
@@ -71,7 +71,7 @@ Section Sigma.
     apply le_lt_trans with (S k); [ rewrite H2; apply le_n | assumption ].
     apply sum_eq; intros; replace (S (low + i)) with (low + S i)%nat.
     reflexivity.
-    ring_nat.
+    ring.
     omega.
     inversion H; [ right; reflexivity | left; assumption ].
   Qed.
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 92284e7d..0a9f7754 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rsqrt_def.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rsqrt_def.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Sumbool.
 Require Import Rbase.
@@ -522,7 +522,7 @@ Proof.
   intro; assumption.
   intro; reflexivity.
   split.
-  intro; elim diff_false_true; assumption.
+  intro feqt;discriminate feqt.
   intro.
   elim n0; assumption.
   unfold Vn in |- *.
@@ -540,7 +540,7 @@ Proof.
   unfold cond_positivity in |- *.
   case (Rle_dec 0 z); intro.
   split.
-  intro; elim diff_true_false; assumption.
+  intro feqt; discriminate feqt.
   intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H7)).
   split.
   intro; auto with real.
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 6e992aa3..b744c788 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rtrigo.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rtrigo.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -466,10 +466,10 @@ Proof.
   unfold x in |- *; replace 0 with (INR 0);
     [ apply le_INR; apply le_O_n | reflexivity ].
   prove_sup0.
-  ring_nat.
+  ring.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma SIN : forall a:R, 0 <= a -> a <= PI -> sin_lb a <= sin a <= sin_ub a.
@@ -1580,10 +1580,14 @@ Lemma cos_eq_0_0 :
 Proof.
   intros x H; rewrite cos_sin in H; generalize (sin_eq_0_0 (PI / INR 2 + x) H);
     intro H2; elim H2; intros x0 H3; exists (x0 - Z_of_nat 1)%Z;
-      rewrite <- Z_R_minus; simpl; ring_simplify;
-(* rewrite (Rmult_comm PI);*) (* old ring compat *)
+      rewrite <- Z_R_minus; simpl.
+unfold INR in H3. field_simplify [(sym_eq H3)]. field.
+(** 
+  ring_simplify.
+ (* rewrite (Rmult_comm PI);*) (* old ring compat *)
         rewrite <- H3; simpl;
-          field; repeat split; discrR.
+          field;repeat split; discrR.
+*)
 Qed.
 
 Lemma cos_eq_0_1 :
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.
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index 854c0b4a..b105ca69 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rtrigo_reg.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rtrigo_reg.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -99,7 +99,7 @@ Proof.
   apply pow_nonzero; assumption.
   replace (2 * S n)%nat with (S (S (2 * n))).
   simpl in |- *; ring.
-  ring_nat.
+  ring.
   apply Rle_ge; apply pow_le; left; apply (cond_pos r).
   apply Rle_ge; apply pow_le; left; apply (cond_pos r).
   apply Rabs_no_R0; apply pow_nonzero; assumption.
@@ -280,7 +280,7 @@ Proof.
   apply pow_nonzero; assumption.
   replace (2 * S n)%nat with (S (S (2 * n))).
   simpl in |- *; ring.
-  ring_nat.
+  ring.
   apply Rle_ge; apply pow_le; left; apply (cond_pos r).
   apply Rle_ge; apply pow_le; left; apply (cond_pos r).
   apply Rabs_no_R0; apply pow_nonzero; assumption.
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 133f2b89..96351618 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: SeqProp.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: SeqProp.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -1265,8 +1265,8 @@ Proof.
   apply lt_le_trans with 1%nat; [ apply lt_O_Sn | assumption ].
   apply INR_fact_neq_0.
   apply not_O_INR; discriminate.
-  ring_nat.
-  ring_nat.
+  ring.
+  ring.
   unfold Vn in |- *; rewrite Rmult_assoc; unfold Rdiv in |- *;
     rewrite (Rmult_comm (Un 0%nat)); rewrite (Rmult_comm (Un n)).
   repeat apply Rmult_le_compat_l.
@@ -1293,8 +1293,8 @@ Proof.
   apply le_INR; omega.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
-  ring_nat.
-  ring_nat.
+  ring.
+  ring.
   intro; unfold Un in |- *; unfold Rdiv in |- *; apply Rmult_lt_0_compat.
   apply pow_lt; assumption.
   apply Rinv_0_lt_compat; apply lt_INR_0; apply neq_O_lt; red in |- *; intro;