mise a jour du nouveau ring et ajout du nouveau field, avant renommages

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7

32 files changed, 409 insertions, 620 deletions

diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 9008b3623..10f6d44f3 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -13,6 +13,7 @@
 
 (* $Id$ *)
 
+Require Import Bool.
 Require Import ZArith.
 Require Import OrderedType.
 Require Import FMapInterface.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index f22f12a4c..47be9d236 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -9,7 +9,7 @@
 (*i $Id$ i*)
 
 Require Export ZArith.
-Require Export ZArithRing.
+Require Export NewZArithRing.
 Require Export Setoid.
 
 (** * Definition of [Q] and basic properties *)
@@ -104,8 +104,10 @@ Proof.
 unfold Qeq in |- *; intros.
 apply Zmult_reg_l with (QDen y). 
 auto with qarith.
-ring; rewrite H; ring.
-rewrite Zmult_assoc; rewrite H0; ring.
+transitivity (Qnum x * QDen y * QDen z)%Z; try ring.
+rewrite H.
+transitivity (Qnum y * QDen z * QDen x)%Z; try ring.
+rewrite H0; ring.
 Qed.
 
 (** Furthermore, this equality is decidable: *)
@@ -167,10 +169,10 @@ Proof.
 unfold Qeq, Qplus; simpl.
 Open Scope Z_scope.
 intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *.
-simpl_mult; ring.
-replace (p1 * ('s2 * 'q2)) with (p1 * 'q2 * 's2) by ring.
+simpl_mult; ring_simplify.
+replace (p1 * 'r2 * 'q2) with (p1 * 'q2 * 'r2) by ring.
 rewrite H.
-replace ('s2 * ('q2 * r1)) with (r1 * 's2 * 'q2) by ring.
+replace (r1 * 'p2 * 'q2 * 's2) with (r1 * 's2 * 'p2 * 'q2) by ring.
 rewrite H0.
 ring.
 Close Scope Z_scope.
@@ -179,7 +181,11 @@ Qed.
 Add Morphism Qopp : Qopp_comp.
 Proof.
 unfold Qeq, Qopp; simpl.
-intros; ring; rewrite H; ring.
+Open Scope Z_scope.
+intros.
+replace (- Qnum x1 * ' Qden x2) with (- (Qnum x1 * ' Qden x2)) by ring.
+rewrite H in |- *;  ring.
+Close Scope Z_scope.
 Qed.
 
 Add Morphism Qminus : Qminus_comp.
@@ -194,10 +200,10 @@ Proof.
 unfold Qeq; simpl.
 Open Scope Z_scope.
 intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *.
-intros; simpl_mult; ring.
-replace ('p2 * (q1 * s1)) with (q1 * 'p2 * s1) by ring.
+intros; simpl_mult; ring_simplify.
+replace (q1 * s1 * 'p2) with (q1 * 'p2 * s1) by ring.
 rewrite <- H.
-replace ('s2 * ('q2 * r1)) with (r1 * 's2 * 'q2) by ring.
+replace (p1 * r1 * 'q2 * 's2) with (r1 * 's2 * p1 * 'q2) by ring.
 rewrite H0.
 ring.
 Close Scope Z_scope.
@@ -579,14 +585,13 @@ unfold Qplus, Qle; intros (x1, x2) (y1, y2) (z1, z2) (t1, t2);
  simpl; simpl_mult.
 Open Scope Z_scope.
 intros.
-match goal with |- ?a <= ?b => ring a; ring b end.
+match goal with |- ?a <= ?b => ring_simplify a b end.
+rewrite Zplus_comm.
 apply Zplus_le_compat.
-replace ('t2 * ('y2 * (z1 * 'x2))) with (z1 * 't2 * ('y2 * 'x2)) by ring.
-replace ('z2 * ('x2 * (t1 * 'y2))) with (t1 * 'z2 * ('y2 * 'x2)) by ring.
-apply Zmult_le_compat_r; auto with zarith.
-replace ('t2 * ('y2 * ('z2 * x1))) with (x1 * 'y2 * ('z2 * 't2)) by ring.
-replace ('z2 * ('x2 * ('t2 * y1))) with (y1 * 'x2 * ('z2 * 't2)) by ring.
-apply Zmult_le_compat_r; auto with zarith.
+match goal with |- ?a <= ?b => ring_simplify z1 t1 ('z2) ('t2) a b end.
+auto with zarith.
+match goal with |- ?a <= ?b => ring_simplify x1 y1 ('x2) ('y2) a b end.
+auto with zarith.
 Close Scope Z_scope.
 Qed.
 
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index 026e850ea..40c310ff4 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -8,6 +8,7 @@
 
 (*i $Id$ i*)
 
+Require Import NewField Field_tac.
 Require Import QArith.
 Require Import Znumtheory.
 Require Import Eqdep_dec.
@@ -493,6 +494,7 @@ intros x y; unfold Qc_eq_bool in |- *; case (Qc_eq_dec x y); simpl in |- *; auto
 intros _ H; inversion H.
 Qed.
 
+(*
 Definition Qcrt : Ring_Theory Qcplus Qcmult 1 0 Qcopp Qc_eq_bool.
 Proof.
 constructor.
@@ -507,17 +509,41 @@ exact Qcmult_plus_distr_l.
 unfold Is_true; intros x y; generalize (Qc_eq_bool_correct x y);
  case (Qc_eq_bool x y); auto.
 Qed.
-
 Add Ring Qc Qcplus Qcmult 1 0 Qcopp Qc_eq_bool Qcrt [ Qcmake ].
+*)
+Definition Qcrt : ring_theory 0 1 Qcplus Qcmult Qcminus Qcopp (eq(A:=Qc)).
+Proof.
+constructor.
+ exact Qcplus_0_l.
+ exact Qcplus_comm.
+ exact Qcplus_assoc.
+ exact Qcmult_1_l.
+ exact Qcmult_comm.
+ exact Qcmult_assoc.
+ exact Qcmult_plus_distr_l.
+ reflexivity.
+ exact Qcplus_opp_r.
+Qed.
 
-(** A field tactic for rational numbers *)
+Definition Qcft :
+  field_theory _ 0%Qc 1%Qc Qcplus Qcmult Qcminus Qcopp Qcdiv Qcinv (eq(A:=Qc)).
+Proof.
+constructor.
+ exact Qcrt.
+ exact Q_apart_0_1.
+ reflexivity.
+ exact Qcmult_inv_l.
+Qed.
 
-Require Import Field.
+Add Field Qcfield : Qcft.
 
+(** A field tactic for rational numbers *)
+
+(*
 Add Field Qc Qcplus Qcmult 1 0 Qcopp Qc_eq_bool Qcinv Qcrt Qcmult_inv_l
  with div:=Qcdiv.
-
-Example test_field : forall x y : Qc, y<>0 -> (x/y)*y = x.
+*)
+Example test_field : (forall x y : Qc, y<>0 -> (x/y)*y = x)%Qc.
 intros.
 field.
 auto.
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index e4b22dd56..5b4d8db03 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -52,8 +52,9 @@ assert ((X1 * Y2)%R = (Y1 * X2)%R).
  unfold X1, X2, Y1, Y2 in |- *; do 2 rewrite <- mult_IZR.
  apply IZR_eq; auto.
 clear H.
-field; auto.
-rewrite <- H0; field; auto.
+field_simplify_eq; auto.
+ring_simplify X1 Y2 (Y2 * X1)%R.
+rewrite H0 in |- *;  ring.
 Qed.
 
 Lemma Rle_Qle : forall x y : Q, (Q2R x <= Q2R y)%R -> x<=y.
@@ -176,16 +177,11 @@ unfold Qinv, Q2R, Qeq in |- *; intros (x1, x2); unfold Qden, Qnum in |- *.
 case x1.
 simpl in |- *; intros; elim H; trivial.
 intros; field; auto.
-apply Rmult_integral_contrapositive; split; auto.
-apply Rmult_integral_contrapositive; split; auto.
-apply Rinv_neq_0_compat; auto.
-intros; field; auto.
-do 2 rewrite <- mult_IZR.
-simpl in |- *; rewrite Pmult_comm; auto.
-apply Rmult_integral_contrapositive; split; auto.
-apply Rmult_integral_contrapositive; split; auto.
-apply not_O_IZR; auto with qarith.
-apply Rinv_neq_0_compat; auto.
+intros; 
+  change (IZR (Zneg x2)) with (- IZR (' x2))%R in |- *;
+  change (IZR (Zneg p)) with (- IZR (' p))%R in |- *;
+  field; (*auto 8 with real.*)
+  repeat split; auto; auto with real.
 Qed.
 
 Lemma Q2R_div :
@@ -210,4 +206,4 @@ Goal forall x y : Q, ~ y==0#1 -> (x/y)*y == x.
 intros; QField.
 intro; apply H; apply eqR_Qeq.
 rewrite H0; unfold Q2R in |- *; simpl in |- *; field; auto with real.
-Abort.
\ No newline at end of file
+Abort.
diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v
index 84a968475..0c4c8399c 100644
--- a/theories/QArith/Qring.v
+++ b/theories/QArith/Qring.v
@@ -8,8 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import Ring.
-Require Export Setoid_ring.
+Require Export Ring.
 Require Export QArith_base.
 
 (** * A ring tactic for rational numbers *)
@@ -22,25 +21,38 @@ intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto.
 intros _ H; inversion H.
 Qed.
 
-Definition Qsrt : Setoid_Ring_Theory Qeq Qplus Qmult 1 0 Qopp Qeq_bool.
+Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq.
 Proof.
 constructor.
+exact Qplus_0_l.
 exact Qplus_comm.
 exact Qplus_assoc.
+exact Qmult_1_l.
 exact Qmult_comm.
 exact Qmult_assoc.
-exact Qplus_0_l.
-exact Qmult_1_l.
-exact Qplus_opp_r.
 exact Qmult_plus_distr_l.
-unfold Is_true; intros x y; generalize (Qeq_bool_correct x y);
- case (Qeq_bool x y); auto.
+reflexivity.
+exact Qplus_opp_r.
 Qed.
 
-Add Setoid Ring Q Qeq Q_Setoid Qplus Qmult 1 0 Qopp Qeq_bool
- Qplus_comp Qmult_comp Qopp_comp Qsrt
- [ Qmake (*inject_Z*)  Zpos 0%Z Zneg xI xO 1%positive ].
-
+Ltac isQcst t :=
+  let t := eval hnf in t in
+  match t with
+    Qmake ?n ?d =>
+      match isZcst n with
+        true => isZcst d
+      | _ => false
+      end
+  | _ => false
+  end.
+
+Ltac Qcst t :=
+  match isQcst t with
+    true => t
+  | _ => NotConstant
+  end.
+
+Add Ring Qring : Qsrt (decidable Qeq_bool_correct, constants [Qcst]).
 (** Exemple of use: *)
 
 Section Examples. 
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index dc365842b..0dfe58552 100644
--- a/theories/Reals/AltSeries.v
+++ b/theories/Reals/AltSeries.v
@@ -88,11 +88,9 @@ rewrite Rplus_0_r;
  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.
-apply INR_eq; rewrite mult_INR; repeat rewrite S_INR; rewrite mult_INR;
- repeat rewrite S_INR; ring.
+ring_nat.
 apply HrecN.
-apply INR_eq; repeat rewrite S_INR; do 2 rewrite mult_INR;
- repeat rewrite S_INR; ring.
+ring_nat.
 Qed.
 
 (* A more general inequality *)
@@ -293,8 +291,7 @@ rewrite (Rmult_comm (INR (2 * S n + 1))); rewrite Rmult_assoc;
 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.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite plus_INR;
- do 2 rewrite mult_INR; repeat rewrite S_INR; ring.
+ring_nat.
 apply not_O_INR; discriminate.
 apply not_O_INR; replace (2 * n + 1)%nat with (S (2 * n));
  [ discriminate | ring ].
@@ -445,4 +442,4 @@ rewrite Rmult_1_l; replace (2 + 1) with 3; [ prove_sup0 | ring ].
 rewrite Rplus_comm; pattern 1 at 1 in |- *; rewrite <- Rplus_0_r;
  apply Rplus_lt_compat_l; prove_sup0.
 assumption.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index 2ec3e2afb..c05ea465d 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -12,6 +12,8 @@ Require Import Rbase.
 Require Import Rbasic_fun.
 Require Import Even.
 Require Import Div2.
+Require Import NewArithRing.
+
 Open Local Scope Z_scope.
 Open Local Scope R_scope.
 
@@ -175,4 +177,4 @@ replace (S n + 0)%nat with (S n); [ apply le_n_Sn | ring ].
 replace (S n + S i)%nat with (S (S n + i)).
 apply le_S; assumption.
 apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; do 2 rewrite S_INR; ring.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v
index a4fa36c62..972482fe8 100644
--- a/theories/Reals/Cauchy_prod.v
+++ b/theories/Reals/Cauchy_prod.v
@@ -171,16 +171,17 @@ apply sum_eq; intros;
      (pred (N - i))).
 replace (S (S (pred (N - i) + i))) with (S N).
 replace (N - pred (N - i))%nat with (S i).
-ring.
+reflexivity.
 rewrite pred_of_minus; apply INR_eq; repeat rewrite minus_INR.
-rewrite S_INR; ring.
+rewrite S_INR; simpl; ring.
 apply le_trans with (pred (pred N)).
 assumption.
 apply le_trans with (pred N); apply le_pred_n.
 apply INR_le; rewrite minus_INR.
 apply Rplus_le_reg_l with (INR i - 1).
-replace (INR i - 1 + INR 1) with (INR i); [ idtac | ring ].
-replace (INR i - 1 + (INR N - INR i)) with (INR N - INR 1); [ idtac | ring ].
+replace (INR i - 1 + INR 1) with (INR i); [ idtac | simpl; ring ].
+replace (INR i - 1 + (INR N - INR i)) with (INR N - INR 1);
+  [ idtac | simpl; ring ].
 rewrite <- minus_INR.
 apply le_INR; apply le_trans with (pred (pred N)).
 assumption.
@@ -219,15 +220,16 @@ apply S_pred with 0%nat; assumption.
 apply le_pred_n.
 apply INR_eq; rewrite pred_of_minus; do 3 rewrite S_INR; rewrite plus_INR;
  repeat rewrite minus_INR.
-ring.
+simpl; ring.
 apply le_trans with (pred (pred N)).
 assumption.
 apply le_trans with (pred N); apply le_pred_n.
 apply INR_le.
 rewrite minus_INR.
 apply Rplus_le_reg_l with (INR i - 1).
-replace (INR i - 1 + INR 1) with (INR i); [ idtac | ring ].
-replace (INR i - 1 + (INR N - INR i)) with (INR N - INR 1); [ idtac | ring ].
+replace (INR i - 1 + INR 1) with (INR i); [ idtac | simpl; ring ].
+replace (INR i - 1 + (INR N - INR i)) with (INR N - INR 1);
+  [ idtac | simpl; ring ].
 rewrite <- minus_INR.
 apply le_INR.
 apply le_trans with (pred (pred N)).
@@ -246,7 +248,7 @@ apply INR_le.
 rewrite pred_of_minus.
 repeat rewrite minus_INR.
 apply Rplus_le_reg_l with (INR i - 1).
-replace (INR i - 1 + INR 1) with (INR i); [ idtac | ring ].
+replace (INR i - 1 + INR 1) with (INR i); [ idtac | simpl; ring ].
 replace (INR i - 1 + (INR N - INR i - INR 1)) with (INR N - INR 1 - INR 1).
 repeat rewrite <- minus_INR.
 apply le_INR.
@@ -259,7 +261,7 @@ rewrite le_plus_minus_r.
 simpl in |- *; assumption.
 apply le_trans with 2%nat; [ apply le_n_Sn | assumption ].
 apply le_trans with 2%nat; [ apply le_n_Sn | assumption ].
-ring.
+simpl; ring.
 apply le_trans with (pred (pred N)).
 assumption.
 apply le_trans with (pred N); apply le_pred_n.
@@ -295,8 +297,7 @@ rewrite
  (sum_plus
     (fun k:nat =>
        sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat)
-         (pred (N - k))) (fun k:nat => An (S k) * Bn (S N)))
- .
+         (pred (N - k))) (fun k:nat => An (S k) * Bn (S N))).
 apply Rplus_eq_compat_l.
 rewrite scal_sum; reflexivity.
 apply sum_eq; intros; rewrite Rplus_comm;
@@ -310,12 +311,12 @@ apply sum_eq; intros.
 replace (S N - S i0)%nat with (N - i0)%nat; [ idtac | reflexivity ].
 replace (S i0 + i)%nat with (S (i0 + i)).
 reflexivity.
-apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; rewrite S_INR; ring.
+apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; rewrite S_INR; simpl; ring.
 cut ((N - i)%nat = pred (S N - i)).
 intro; rewrite H5; reflexivity.
 rewrite pred_of_minus.
 apply INR_eq; repeat rewrite minus_INR.
-rewrite S_INR; ring.
+rewrite S_INR; simpl; ring.
 apply le_trans with N.
 apply le_trans with (pred N).
 assumption.
@@ -328,7 +329,7 @@ apply le_n_S.
 apply le_trans with (pred N).
 assumption.
 apply le_pred_n.
-apply INR_eq; rewrite S_INR; rewrite plus_INR; ring.
+apply INR_eq; rewrite S_INR; rewrite plus_INR; simpl; ring.
 apply le_trans with N.
 apply le_trans with (pred N).
 assumption.
@@ -351,7 +352,7 @@ assumption.
 apply le_pred_n.
 rewrite pred_of_minus.
 apply INR_eq; repeat rewrite minus_INR.
-repeat rewrite S_INR; ring.
+repeat rewrite S_INR; simpl; ring.
 apply le_trans with N.
 apply le_trans with (pred N).
 assumption.
@@ -364,7 +365,7 @@ apply le_n_S.
 apply le_trans with (pred N).
 assumption.
 apply le_pred_n.
-apply INR_eq; rewrite S_INR; rewrite plus_INR; ring.
+apply INR_eq; rewrite S_INR; rewrite plus_INR; simpl; ring.
 apply le_trans with N.
 apply le_trans with (pred N).
 assumption.
@@ -396,13 +397,13 @@ replace (pred (N - S i)) with (pred (pred (N - i))).
 apply sum_eq; intros.
 replace (i0 + S i)%nat with (S (i0 + i)).
 reflexivity.
-apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; rewrite S_INR; ring.
+apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; rewrite S_INR; simpl; ring.
 cut (pred (N - i) = (N - S i)%nat).
 intro; rewrite H5; reflexivity.
 rewrite pred_of_minus.
 apply INR_eq.
 repeat rewrite minus_INR.
-repeat rewrite S_INR; ring.
+repeat rewrite S_INR; simpl; ring.
 apply le_trans with (S (pred (pred N))).
 apply le_n_S; assumption.
 replace (S (pred (pred N))) with (pred N).
@@ -426,7 +427,7 @@ apply le_trans with (pred (pred N)).
 assumption.
 apply le_pred_n.
 symmetry  in |- *; apply S_pred with 0%nat; assumption.
-apply INR_eq; rewrite S_INR; rewrite plus_INR; ring.
+apply INR_eq; rewrite S_INR; rewrite plus_INR; simpl; ring.
 apply le_trans with (pred (pred N)).
 assumption.
 apply le_trans with (pred N); apply le_pred_n.
@@ -448,11 +449,11 @@ cut ((N - pred N)%nat = 1%nat).
 intro; rewrite H2; reflexivity.
 rewrite pred_of_minus.
 apply INR_eq; repeat rewrite minus_INR.
-ring.
+simpl; ring.
 apply lt_le_S; assumption.
 rewrite <- pred_of_minus; apply le_pred_n.
 simpl in |- *; symmetry  in |- *; apply S_pred with 0%nat; assumption.
 inversion H.
 left; reflexivity.
 right; apply lt_le_trans with 1%nat; [ apply lt_n_Sn | exact H1 ].
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index d3040246a..c81ac1acf 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -208,10 +208,7 @@ replace (2 * N)%nat with (S (N + pred N)).
 apply le_n_S.
 apply plus_le_compat_l; assumption.
 rewrite pred_of_minus.
-apply INR_eq; rewrite S_INR; rewrite plus_INR; rewrite mult_INR;
- rewrite minus_INR.
-repeat rewrite S_INR; ring.
-apply lt_le_S; assumption.
+omega.
 apply Rle_trans with
  (sum_f_R0
     (fun k:nat =>
@@ -234,31 +231,7 @@ unfold Rdiv in |- *;
 apply Rmult_le_compat_l.
 left; apply Rinv_0_lt_compat; apply INR_fact_lt_0.
 apply C_maj.
-apply (fun m n p:nat => mult_le_compat_l p n m).
-apply le_n_S.
-apply plus_le_compat_r.
-apply le_trans with (pred (N - n)).
-assumption.
-apply le_S_n.
-replace (S (pred (N - n))) with (N - n)%nat.
-apply le_trans with N.
-apply (fun p n m:nat => plus_le_reg_l n m p) with n.
-rewrite <- le_plus_minus.
-apply le_plus_r.
-apply le_trans with (pred N).
-assumption.
-apply le_pred_n.
-apply le_n_Sn.
-apply S_pred with 0%nat.
-apply plus_lt_reg_l with n.
-rewrite <- le_plus_minus.
-replace (n + 0)%nat with n; [ idtac | ring ].
-apply le_lt_trans with (pred N).
-assumption.
-apply lt_pred_n_n; assumption.
-apply le_trans with (pred N).
-assumption.
-apply le_pred_n.
+omega.
 right.
 unfold Rdiv in |- *; rewrite Rmult_comm.
 unfold Binomial.C in |- *.
@@ -270,9 +243,7 @@ rewrite Rinv_mult_distr.
 unfold Rsqr in |- *; reflexivity.
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
-apply INR_eq; rewrite S_INR; rewrite minus_INR.
-rewrite mult_INR; repeat rewrite S_INR; rewrite plus_INR; ring.
-apply le_n_2n.
+omega.
 apply INR_fact_neq_0.
 unfold Rdiv in |- *; rewrite Rmult_comm.
 unfold Binomial.C in |- *.
@@ -282,57 +253,7 @@ rewrite Rmult_1_l.
 replace (2 * S (N + n) - 2 * S (n0 + n))%nat with (2 * (N - n0))%nat.
 rewrite mult_INR.
 reflexivity.
-apply INR_eq; rewrite minus_INR.
-do 3 rewrite mult_INR; repeat rewrite S_INR; do 2 rewrite plus_INR;
- rewrite minus_INR.
-ring.
-apply le_trans with (pred (N - n)).
-assumption.
-apply le_S_n.
-replace (S (pred (N - n))) with (N - n)%nat.
-apply le_trans with N.
-apply (fun p n m:nat => plus_le_reg_l n m p) with n.
-rewrite <- le_plus_minus.
-apply le_plus_r.
-apply le_trans with (pred N).
-assumption.
-apply le_pred_n.
-apply le_n_Sn.
-apply S_pred with 0%nat.
-apply plus_lt_reg_l with n.
-rewrite <- le_plus_minus.
-replace (n + 0)%nat with n; [ idtac | ring ].
-apply le_lt_trans with (pred N).
-assumption.
-apply lt_pred_n_n; assumption.
-apply le_trans with (pred N).
-assumption.
-apply le_pred_n.
-apply (fun m n p:nat => mult_le_compat_l p n m).
-apply le_n_S.
-apply plus_le_compat_r.
-apply le_trans with (pred (N - n)).
-assumption.
-apply le_S_n.
-replace (S (pred (N - n))) with (N - n)%nat.
-apply le_trans with N.
-apply (fun p n m:nat => plus_le_reg_l n m p) with n.
-rewrite <- le_plus_minus.
-apply le_plus_r.
-apply le_trans with (pred N).
-assumption.
-apply le_pred_n.
-apply le_n_Sn.
-apply S_pred with 0%nat.
-apply plus_lt_reg_l with n.
-rewrite <- le_plus_minus.
-replace (n + 0)%nat with n; [ idtac | ring ].
-apply le_lt_trans with (pred N).
-assumption.
-apply lt_pred_n_n; assumption.
-apply le_trans with (pred N).
-assumption.
-apply le_pred_n.
+omega.
 apply INR_fact_neq_0.
 apply Rle_trans with
  (sum_f_R0 (fun k:nat => INR N / INR (fact (S N)) * C ^ (4 * N)) (pred N)).
@@ -352,24 +273,8 @@ unfold C in |- *; apply RmaxLess1.
 apply Rle_trans with (Rsqr (/ INR (fact (S (N + n)))) * INR N).
 apply Rmult_le_compat_l.
 apply Rle_0_sqr.
-replace (S (pred (N - n))) with (N - n)%nat.
 apply le_INR.
-apply (fun p n m:nat => plus_le_reg_l n m p) with n.
-rewrite <- le_plus_minus.
-apply le_plus_r.
-apply le_trans with (pred N).
-assumption.
-apply le_pred_n.
-apply S_pred with 0%nat.
-apply plus_lt_reg_l with n.
-rewrite <- le_plus_minus.
-replace (n + 0)%nat with n; [ idtac | ring ].
-apply le_lt_trans with (pred N).
-assumption.
-apply lt_pred_n_n; assumption.
-apply le_trans with (pred N).
-assumption.
-apply le_pred_n.
+omega.
 rewrite Rmult_comm; unfold Rdiv in |- *; apply Rmult_le_compat_l.
 apply pos_INR.
 apply Rle_trans with (/ INR (fact (S (N + n)))).
@@ -549,31 +454,7 @@ replace (2 * S (S (N + n)))%nat with
  (2 * (N - n0) + 1 + (2 * S (n0 + n) + 1))%nat.
 repeat rewrite pow_add.
 ring.
-apply INR_eq; repeat rewrite plus_INR; do 3 rewrite mult_INR.
-rewrite minus_INR.
-repeat rewrite S_INR; do 2 rewrite plus_INR; ring.
-apply le_trans with (pred (N - n)).
-exact H1.
-apply le_S_n.
-replace (S (pred (N - n))) with (N - n)%nat.
-apply le_trans with N.
-apply (fun p n m:nat => plus_le_reg_l n m p) with n.
-rewrite <- le_plus_minus.
-apply le_plus_r.
-apply le_trans with (pred N).
-assumption.
-apply le_pred_n.
-apply le_n_Sn.
-apply S_pred with 0%nat.
-apply plus_lt_reg_l with n.
-rewrite <- le_plus_minus.
-replace (n + 0)%nat with n; [ idtac | ring ].
-apply le_lt_trans with (pred N).
-assumption.
-apply lt_pred_n_n; assumption.
-apply le_trans with (pred N).
-assumption.
-apply le_pred_n.
+omega.
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
 apply Rle_ge; left; apply Rinv_0_lt_compat.
@@ -602,8 +483,7 @@ apply plus_le_compat_l.
 apply le_trans with (pred N).
 assumption.
 apply le_pred_n.
-apply INR_eq; do 2 rewrite S_INR; rewrite plus_INR; rewrite mult_INR.
-repeat rewrite S_INR; ring.
+ring_nat.
 apply Rle_trans with
  (sum_f_R0
     (fun k:nat =>
@@ -632,33 +512,8 @@ apply C_maj.
 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.
-apply INR_eq; rewrite S_INR; rewrite plus_INR; do 2 rewrite mult_INR;
- repeat rewrite S_INR; rewrite plus_INR; ring.
-apply (fun m n p:nat => mult_le_compat_l p n m).
-repeat apply le_n_S.
-apply plus_le_compat_r.
-apply le_trans with (pred (N - n)).
-assumption.
-apply le_S_n.
-replace (S (pred (N - n))) with (N - n)%nat.
-apply le_trans with N.
-apply (fun p n m:nat => plus_le_reg_l n m p) with n.
-rewrite <- le_plus_minus.
-apply le_plus_r.
-apply le_trans with (pred N).
-assumption.
-apply le_pred_n.
-apply le_n_Sn.
-apply S_pred with 0%nat.
-apply plus_lt_reg_l with n.
-rewrite <- le_plus_minus.
-replace (n + 0)%nat with n; [ idtac | ring ].
-apply le_lt_trans with (pred N).
-assumption.
-apply lt_pred_n_n; assumption.
-apply le_trans with (pred N).
-assumption.
-apply le_pred_n.
+ring_nat.
+omega.
 right.
 unfold Rdiv in |- *; rewrite Rmult_comm.
 unfold Binomial.C in |- *.
@@ -670,9 +525,7 @@ rewrite Rinv_mult_distr.
 unfold Rsqr in |- *; reflexivity.
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
-apply INR_eq; do 2 rewrite S_INR; rewrite minus_INR.
-rewrite mult_INR; repeat rewrite S_INR; rewrite plus_INR; ring.
-apply le_n_2n.
+omega.
 apply INR_fact_neq_0.
 unfold Rdiv in |- *; rewrite Rmult_comm.
 unfold Binomial.C in |- *.
@@ -683,62 +536,7 @@ replace (2 * S (S (N + n)) - (2 * S (n0 + n) + 1))%nat with
  (2 * (N - n0) + 1)%nat.
 rewrite mult_INR.
 reflexivity.
-apply INR_eq; rewrite minus_INR.
-do 2 rewrite plus_INR; do 3 rewrite mult_INR; repeat rewrite S_INR;
- do 2 rewrite plus_INR; rewrite minus_INR.
-ring.
-apply le_trans with (pred (N - n)).
-assumption.
-apply le_S_n.
-replace (S (pred (N - n))) with (N - n)%nat.
-apply le_trans with N.
-apply (fun p n m:nat => plus_le_reg_l n m p) with n.
-rewrite <- le_plus_minus.
-apply le_plus_r.
-apply le_trans with (pred N).
-assumption.
-apply le_pred_n.
-apply le_n_Sn.
-apply S_pred with 0%nat.
-apply plus_lt_reg_l with n.
-rewrite <- le_plus_minus.
-replace (n + 0)%nat with n; [ idtac | ring ].
-apply le_lt_trans with (pred N).
-assumption.
-apply lt_pred_n_n; assumption.
-apply le_trans with (pred N).
-assumption.
-apply le_pred_n.
-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.
-apply INR_eq; rewrite S_INR; rewrite plus_INR; do 2 rewrite mult_INR;
- repeat rewrite S_INR; rewrite plus_INR; ring.
-apply (fun m n p:nat => mult_le_compat_l p n m).
-repeat apply le_n_S.
-apply plus_le_compat_r.
-apply le_trans with (pred (N - n)).
-assumption.
-apply le_S_n.
-replace (S (pred (N - n))) with (N - n)%nat.
-apply le_trans with N.
-apply (fun p n m:nat => plus_le_reg_l n m p) with n.
-rewrite <- le_plus_minus.
-apply le_plus_r.
-apply le_trans with (pred N).
-assumption.
-apply le_pred_n.
-apply le_n_Sn.
-apply S_pred with 0%nat.
-apply plus_lt_reg_l with n.
-rewrite <- le_plus_minus.
-replace (n + 0)%nat with n; [ idtac | ring ].
-apply le_lt_trans with (pred N).
-assumption.
-apply lt_pred_n_n; assumption.
-apply le_trans with (pred N).
-assumption.
-apply le_pred_n.
+omega.
 apply INR_fact_neq_0.
 apply Rle_trans with
  (sum_f_R0 (fun k:nat => INR N / INR (fact (S (S N))) * C ^ (4 * S N))
@@ -761,22 +559,8 @@ apply Rmult_le_compat_l.
 apply Rle_0_sqr.
 replace (S (pred (N - n))) with (N - n)%nat.
 apply le_INR.
-apply (fun p n m:nat => plus_le_reg_l n m p) with n.
-rewrite <- le_plus_minus.
-apply le_plus_r.
-apply le_trans with (pred N).
-assumption.
-apply le_pred_n.
-apply S_pred with 0%nat.
-apply plus_lt_reg_l with n.
-rewrite <- le_plus_minus.
-replace (n + 0)%nat with n; [ idtac | ring ].
-apply le_lt_trans with (pred N).
-assumption.
-apply lt_pred_n_n; assumption.
-apply le_trans with (pred N).
-assumption.
-apply le_pred_n.
+omega.
+omega.
 rewrite Rmult_comm; unfold Rdiv in |- *; apply Rmult_le_compat_l.
 apply pos_INR.
 apply Rle_trans with (/ INR (fact (S (S (N + n))))).
@@ -806,8 +590,7 @@ rewrite <- Rinv_l_sym.
 rewrite Rmult_1_r.
 apply le_INR.
 apply fact_le.
-repeat apply le_n_S.
-apply le_plus_l.
+omega.
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
 rewrite sum_cte.
@@ -1058,4 +841,4 @@ intro.
 apply S_pred with 0%nat; assumption.
 apply lt_le_trans with N; assumption. 
 unfold N in |- *; apply lt_O_Sn.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index ba108e95e..a3dbca23d 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -83,7 +83,6 @@ replace
             ((-1) ^ (n - l) / INR (fact (2 * (n - l) + 1)) *
              y ^ (2 * (n - l) + 1))) (pred (n - k))) (
     pred n)) with (Reste2 x y n).
-ring.
 replace
  (sum_f_R0
     (fun k:nat =>
@@ -98,7 +97,7 @@ replace
        sum_f_R0
          (fun l:nat => C (2 * k) (2 * l) * x ^ (2 * l) * y ^ (2 * (k - l))) k)
     (S n)).
-set
+pose
  (sin_nnn :=
   fun n:nat =>
     match n with
@@ -109,8 +108,10 @@ set
           (fun l:nat =>
              C (2 * S p) (S (2 * l)) * x ^ S (2 * l) * y ^ S (2 * (p - l))) p
     end).
+ring_simplify.
 replace
- (-
+(* (-   old ring compat *)
+ (-1 *
   sum_f_R0
     (fun k:nat =>
        sum_f_R0
@@ -123,19 +124,13 @@ unfold C1 in |- *.
 apply sum_eq; intros.
 induction  i as [| i Hreci].
 simpl in |- *.
-rewrite Rplus_0_l.
-replace (C 0 0) with 1.
-unfold Rdiv in |- *; rewrite Rinv_1.
-ring.
-unfold C in |- *.
-rewrite <- minus_n_n.
-simpl in |- *.
-unfold Rdiv in |- *; rewrite Rmult_1_r; rewrite Rinv_1; ring.
+unfold C in |- *; simpl in |- *.
+field; discrR.
 unfold sin_nnn in |- *.
 rewrite <- Rmult_plus_distr_l.
 apply Rmult_eq_compat_l.
 rewrite binomial.
-set (Wn := fun i0:nat => C (2 * S i) i0 * x ^ i0 * y ^ (2 * S i - i0)).
+pose (Wn := fun i0:nat => C (2 * S i) i0 * x ^ i0 * y ^ (2 * S i - i0)).
 replace
  (sum_f_R0
     (fun l:nat => C (2 * S i) (2 * l) * x ^ (2 * l) * y ^ (2 * (S i - l)))
@@ -145,42 +140,39 @@ 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.
+(*rewrite Rplus_comm.*) (* compatibility old ring... *)
 apply sum_decomposition.
 apply sum_eq; intros.
 unfold Wn in |- *.
 apply Rmult_eq_compat_l.
 replace (2 * S i - S (2 * i0))%nat with (S (2 * (i - i0))).
 reflexivity.
-apply INR_eq.
-rewrite S_INR; rewrite mult_INR.
-repeat rewrite minus_INR.
-rewrite mult_INR; repeat rewrite S_INR.
-rewrite mult_INR; repeat rewrite S_INR; ring.
-replace (2 * S i)%nat with (S (S (2 * i))).
-apply le_n_S.
-apply le_trans with (2 * i)%nat.
-apply (fun m n p:nat => mult_le_compat_l p n m); assumption.
-apply le_n_Sn.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR;
- ring.
-assumption.
+omega.
 apply sum_eq; intros.
 unfold Wn in |- *.
 apply Rmult_eq_compat_l.
 replace (2 * S i - 2 * i0)%nat with (2 * (S i - i0))%nat.
 reflexivity.
-apply INR_eq.
-rewrite mult_INR.
-repeat rewrite minus_INR.
-rewrite mult_INR; repeat rewrite S_INR.
-rewrite mult_INR; repeat rewrite S_INR; ring.
-apply (fun m n p:nat => mult_le_compat_l p n m); assumption.
-assumption.
-rewrite <- (Ropp_involutive (sum_f_R0 sin_nnn (S n))).
-apply Ropp_eq_compat.
-replace (- sum_f_R0 sin_nnn (S n)) with (-1 * sum_f_R0 sin_nnn (S n));
- [ idtac | ring ].
+omega.
+replace (sum_f_R0 sin_nnn (S n)) with (-1 * (-1 * sum_f_R0 sin_nnn (S n))).
+(*replace (* compatibility old ring... *)
+ (-
+  sum_f_R0
+    (fun k:nat =>
+       sum_f_R0
+         (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) with
+ (-1 *
+  sum_f_R0
+    (fun k:nat =>
+       sum_f_R0
+         (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.
 rewrite scal_sum.
 rewrite decomp_sum.
 replace (sin_nnn 0%nat) with 0.
@@ -218,25 +210,13 @@ replace (S (2 * i0)) with (2 * i0 + 1)%nat;
  [ apply Rmult_eq_compat_l | ring ].
 replace (2 * S i - (2 * i0 + 1))%nat with (2 * (i - i0) + 1)%nat.
 reflexivity.
-apply INR_eq.
-rewrite plus_INR; rewrite mult_INR; repeat rewrite minus_INR.
-rewrite plus_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; ring.
-replace (2 * i0 + 1)%nat with (S (2 * i0)).
-replace (2 * S i)%nat with (S (S (2 * i))).
-apply le_n_S.
-apply le_trans with (2 * i)%nat.
-apply (fun m n p:nat => mult_le_compat_l p n m); assumption.
-apply le_n_Sn.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR;
- ring.
-apply INR_eq; rewrite S_INR; rewrite plus_INR; rewrite mult_INR;
- repeat rewrite S_INR; ring.
-assumption.
+omega.
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
 reflexivity.
 apply lt_O_Sn.
+ring.
 apply sum_eq; intros.
 rewrite scal_sum.
 apply sum_eq; intros.
@@ -259,11 +239,7 @@ rewrite Rmult_1_l.
 rewrite Rinv_mult_distr.
 replace (2 * i - 2 * i0)%nat with (2 * (i - i0))%nat.
 reflexivity.
-apply INR_eq.
-rewrite mult_INR; repeat rewrite minus_INR.
-do 2 rewrite mult_INR; repeat rewrite S_INR; ring.
-apply (fun m n p:nat => mult_le_compat_l p n m); assumption.
-assumption.
+omega.
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index 1c41aeb0c..519593381 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -12,7 +12,7 @@ Require Import RIneq.
 Require Import Omega. Open Local Scope R_scope.
 
 Lemma Rlt_R0_R2 : 0 < 2.
-replace 2 with (INR 2); [ apply lt_INR_0; apply lt_O_Sn | reflexivity ].
+change 2 with (INR 2); apply lt_INR_0; apply lt_O_Sn.
 Qed.
 
 Lemma Rplus_lt_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x + y.
@@ -36,17 +36,14 @@ Ltac discrR :=
   try
    match goal with
    |  |- (?X1 <> ?X2) =>
-       replace 2 with (IZR 2);
-        [ replace 1 with (IZR 1);
-           [ replace 0 with (IZR 0);
-              [ repeat
-                 rewrite <- plus_IZR ||
-                   rewrite <- mult_IZR ||
-                     rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus;
-                 apply IZR_neq; try discriminate
-              | reflexivity ]
-           | reflexivity ]
-        | reflexivity ]
+       change 2 with (IZR 2);
+       change 1 with (IZR 1);
+       change 0 with (IZR 0);
+       repeat
+         rewrite <- plus_IZR ||
+           rewrite <- mult_IZR ||
+           rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus;
+       apply IZR_neq; try discriminate
    end.
 
 Ltac prove_sup0 :=
@@ -60,17 +57,13 @@ Ltac prove_sup0 :=
   end.
 
 Ltac omega_sup :=
-  replace 2 with (IZR 2);
-   [ replace 1 with (IZR 1);
-      [ replace 0 with (IZR 0);
-         [ repeat
-            rewrite <- plus_IZR ||
-              rewrite <- mult_IZR ||
-                rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus; 
-            apply IZR_lt; omega
-         | reflexivity ]
-      | reflexivity ]
-   | reflexivity ].
+  change 2 with (IZR 2);
+  change 1 with (IZR 1);
+  change 0 with (IZR 0);
+  repeat
+    rewrite <- plus_IZR ||
+      rewrite <- mult_IZR || rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus; 
+  apply IZR_lt; omega.
   
 Ltac prove_sup :=
   match goal with
@@ -84,14 +77,10 @@ Ltac prove_sup :=
   end.
 
 Ltac Rcompute :=
-  replace 2 with (IZR 2);
-   [ replace 1 with (IZR 1);
-      [ replace 0 with (IZR 0);
-         [ repeat
-            rewrite <- plus_IZR ||
-              rewrite <- mult_IZR ||
-                rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus; 
-            apply IZR_eq; try reflexivity
-         | reflexivity ]
-      | reflexivity ]
-   | reflexivity ].
\ No newline at end of file
+  change 2 with (IZR 2);
+  change 1 with (IZR 1);
+  change 0 with (IZR 0);
+  repeat
+    rewrite <- plus_IZR ||
+      rewrite <- mult_IZR || rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus; 
+  apply IZR_eq; try reflexivity.
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index b0849be4a..a44bf1456 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -83,8 +83,7 @@ intro; induction  N as [| N HrecN].
 reflexivity.
 replace (2 * S N)%nat with (S (S (2 * N))).
 simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR;
- ring.
+ring_nat.
 Qed.
 
 Lemma div2_S_double : forall N:nat, div2 (S (2 * N)) = N.
@@ -92,8 +91,7 @@ intro; induction  N as [| N HrecN].
 reflexivity.
 replace (2 * S N)%nat with (S (S (2 * N))).
 simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR;
- ring.
+ring_nat.
 Qed.
 
 Lemma div2_not_R0 : forall N:nat, (1 < N)%nat -> (0 < div2 N)%nat.
@@ -315,7 +313,7 @@ ring.
 replace N with (N0 + N0)%nat.
 symmetry  in |- *; apply minus_plus.
 rewrite H4.
-apply INR_eq; rewrite plus_INR; rewrite mult_INR; do 2 rewrite S_INR; ring.
+ring.
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
@@ -362,8 +360,7 @@ apply H.
 apply le_trans with (pred N).
 apply H0.
 apply le_pred_n.
-apply INR_eq; rewrite H4.
-do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR; ring.
+rewrite H4; ring_nat.
 cut (S N = (2 * S N0)%nat).
 intro.
 replace (C (S N) (S N0) / INR (fact (S N))) with (/ Rsqr (INR (fact (S N0)))).
@@ -384,8 +381,7 @@ apply INR_fact_neq_0.
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
-apply INR_eq; rewrite H4; do 2 rewrite S_INR; do 2 rewrite mult_INR;
- repeat rewrite S_INR; ring.
+rewrite H4; ring_nat.
 unfold C, Rdiv in |- *.
 rewrite (Rmult_comm (INR (fact (S N)))).
 rewrite Rmult_assoc; rewrite <- Rinv_r_sym.
@@ -491,8 +487,7 @@ rewrite Rmult_1_r.
 simpl in |- *.
 pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
  apply Rlt_0_1.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR;
- ring.
+ring_nat.
 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).
@@ -506,23 +501,14 @@ replace (pred (S (S (2 * pred N0)))) with (S (2 * pred N0)).
 rewrite div2_S_double.
 apply S_pred with 0%nat; apply H3.
 reflexivity.
-replace N0 with (S (pred N0)).
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR;
- ring.
-symmetry  in |- *; apply S_pred with 0%nat; apply H3.
-rewrite H2 in H.
-apply neq_O_lt.
-red in |- *; intro.
-rewrite <- H3 in H.
-simpl in H.
-elim (lt_n_O _ H).
+omega.
+omega.
 rewrite H2.
 replace (pred (S (2 * N0))) with (2 * N0)%nat; [ idtac | reflexivity ].
 replace (S (S (2 * N0))) with (2 * S N0)%nat.
 do 2 rewrite div2_double.
 reflexivity.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR;
- ring.
+ring_nat.
 apply S_pred with 0%nat; apply H.
 Qed.
 
@@ -575,28 +561,15 @@ intro.
 rewrite H6.
 replace (pred (2 * N1)) with (S (2 * pred N1)).
 rewrite div2_S_double.
-replace (S (pred N1)) with N1.
-apply INR_le.
-right.
-do 3 rewrite mult_INR; repeat rewrite S_INR; ring.
-apply S_pred with 0%nat; apply H7.
-replace (2 * N1)%nat with (S (S (2 * pred N1))).
-reflexivity.
-pattern N1 at 2 in |- *; replace N1 with (S (pred N1)).
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR;
- ring.
-symmetry  in |- *; apply S_pred with 0%nat; apply H7.
-apply INR_lt.
-apply Rmult_lt_reg_l with (INR 2).
-simpl in |- *; prove_sup0.
-rewrite Rmult_0_r; rewrite <- mult_INR.
-apply lt_INR_0.
-rewrite <- H6.
+omega.
+omega.
+assert (0 < n)%nat.
 apply lt_le_trans with 2%nat.
 apply lt_O_Sn.
 apply le_trans with (max (2 * S N0) 2).
 apply le_max_r.
 apply H3.
+omega.
 rewrite H6.
 replace (pred (S (2 * N1))) with (2 * N1)%nat.
 rewrite div2_double.
@@ -604,9 +577,8 @@ replace (4 * S N1)%nat with (2 * (2 * S N1))%nat.
 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.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR;
- ring.
-ring.
+ring_nat.
+ring_nat.
 reflexivity.
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
@@ -643,8 +615,7 @@ apply S_pred with 0%nat; apply H8.
 replace (2 * N1)%nat with (S (S (2 * pred N1))).
 reflexivity.
 pattern N1 at 2 in |- *; replace N1 with (S (pred N1)).
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR;
- ring.
+ring_nat.
 symmetry  in |- *; apply S_pred with 0%nat; apply H8.
 apply INR_lt.
 apply Rmult_lt_reg_l with (INR 2).
@@ -662,8 +633,7 @@ replace (pred (S (2 * N1))) with (2 * N1)%nat.
 rewrite div2_double.
 replace (2 * S N1)%nat with (S (S (2 * N1))).
 apply le_n_Sn.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR;
- ring.
+ring_nat.
 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 9fe077a4e..74f93cb87 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -262,8 +262,7 @@ rewrite (tech5 An (S (2 * S N))).
 rewrite (tech5 An (2 * S N)).
 rewrite <- HrecN.
 ring.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR.
-ring.
+ring_nat.
 Qed.
 
 Lemma sum_Rle :
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 70bc25eff..3b5d241fa 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -13,9 +13,9 @@
 (***************************************************************************)
 
 Require Export Raxioms.
-Require Export ZArithRing.
+Require Export NewZArithRing.
 Require Import Omega.
-Require Export Field.
+Require Export Field_tac. Import NewField.
 
 Open Local Scope Z_scope.
 Open Local Scope R_scope.
@@ -26,25 +26,105 @@ Implicit Type r : R.
 (**       Instantiating Ring tactic on reals                               *)
 (***************************************************************************)
 
-Lemma RTheory : Ring_Theory Rplus Rmult 1 0 Ropp (fun x y:R => false).
-  split.
-  exact Rplus_comm.
-  symmetry  in |- *; apply Rplus_assoc.
-  exact Rmult_comm.
-  symmetry  in |- *; apply Rmult_assoc.
-  intro; apply Rplus_0_l.
-  intro; apply Rmult_1_l.
-  exact Rplus_opp_r.
-  intros.
-  rewrite Rmult_comm.
-  rewrite (Rmult_comm n p).
-  rewrite (Rmult_comm m p).
-  apply Rmult_plus_distr_l.
-  intros; contradiction.
-Defined.
-
-Add Field R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RTheory Rinv_l
- with minus := Rminus div := Rdiv.
+Lemma RTheory : ring_theory 0 1 Rplus Rmult Rminus Ropp (eq (A:=R)).
+Proof.
+constructor.
+ intro; apply Rplus_0_l.
+ exact Rplus_comm.
+ symmetry  in |- *; apply Rplus_assoc.
+ intro; apply Rmult_1_l.
+ exact Rmult_comm.
+ symmetry  in |- *; apply Rmult_assoc.
+ intros m n p.
+   rewrite Rmult_comm in |- *.
+   rewrite (Rmult_comm n p) in |- *.
+   rewrite (Rmult_comm m p) in |- *.
+   apply Rmult_plus_distr_l.
+ reflexivity.
+ exact Rplus_opp_r.
+Qed.
+
+Lemma Rfield :
+  field_theory R 0 1 Rplus Rmult Rminus Ropp Rdiv Rinv (eq(A:=R)).
+Proof.
+constructor.
+ exact RTheory.
+ exact R1_neq_R0.
+ reflexivity.
+ exact Rinv_l.
+Qed.
+
+Lemma Rlt_n_Sn : forall x, x < x + 1.
+Proof.
+intro.
+elim archimed with x; intros.
+destruct H0.
+ apply Rlt_trans with (IZR (up x)); trivial.
+    replace (IZR (up x)) with (x + (IZR (up x) - x))%R.
+  apply Rplus_lt_compat_l; trivial.
+  unfold Rminus in |- *.
+    rewrite (Rplus_comm (IZR (up x)) (- x)) in |- *.
+    rewrite <- Rplus_assoc in |- *.
+    rewrite Rplus_opp_r in |- *.
+    apply Rplus_0_l.
+ elim H0.
+   unfold Rminus in |- *.
+   rewrite (Rplus_comm (IZR (up x)) (- x)) in |- *.
+   rewrite <- Rplus_assoc in |- *.
+   rewrite Rplus_opp_r in |- *.
+   rewrite Rplus_0_l in |- *; trivial.
+Qed.
+
+Notation Rset := (Eqsth R).
+Notation Rext := (Eq_ext Rplus Rmult Ropp).
+
+Lemma Rlt_0_2 : 0 < 2.
+apply Rlt_trans with (0 + 1).
+ apply Rlt_n_Sn.
+ rewrite Rplus_comm in |- *.
+   apply Rplus_lt_compat_l.
+    replace 1 with (0 + 1).
+  apply Rlt_n_Sn.
+  apply Rplus_0_l.
+Qed.
+
+Lemma Rgen_phiPOS : forall x, ZRing_th.gen_phiPOS1 1 Rplus Rmult x > 0.
+unfold Rgt in |- *.
+induction x; simpl in |- *; intros.
+ apply Rlt_trans with (1 + 0).
+  rewrite Rplus_comm in |- *.
+    apply Rlt_n_Sn.
+  apply Rplus_lt_compat_l.
+    rewrite <- (Rmul_0_l Rset Rext RTheory 2) in |- *.
+    rewrite Rmult_comm in |- *.
+    apply Rmult_lt_compat_l.
+   apply Rlt_0_2.
+   trivial.
+ rewrite <- (Rmul_0_l Rset Rext RTheory 2) in |- *.
+   rewrite Rmult_comm in |- *.
+   apply Rmult_lt_compat_l.
+  apply Rlt_0_2.
+  trivial.
+  replace 1 with (0 + 1).
+  apply Rlt_n_Sn.
+  apply Rplus_0_l.
+Qed.
+
+
+Lemma Rgen_phiPOS_not_0 : forall x, ZRing_th.gen_phiPOS1 1 Rplus Rmult x <> 0.
+red in |- *; intros.
+specialize (Rgen_phiPOS x).
+rewrite H in |- *; intro.
+apply (Rlt_asym 0 0); trivial.
+Qed.
+
+Lemma Zeq_bool_complete : forall x y, 
+  ZRing_th.gen_phiZ 0%R 1%R Rplus Rmult Ropp x =
+  ZRing_th.gen_phiZ 0%R 1%R Rplus Rmult Ropp y ->
+  Zeq_bool x y = true.
+Proof gen_phiZ_complete _ _ _ _ _ _ _ _ _ _ Rset Rext Rfield Rgen_phiPOS_not_0.
+
+Add Field RField : Rfield (infinite Zeq_bool_complete).
 
 (**************************************************************************)
 (**  Relation between orders and equality                                 *)
@@ -259,7 +339,7 @@ Qed.
 (*********************************************************)
 
 Lemma Rplus_ne : forall r, r + 0 = r /\ 0 + r = r.
-intro; split; ring.
+split; ring.
 Qed.
 Hint Resolve Rplus_ne: real v62.
 
@@ -270,15 +350,16 @@ Hint Resolve Rplus_0_r: real.
 
 (**********)
 Lemma Rplus_opp_l : forall r, - r + r = 0.
-  intro; ring.
+intro; ring.
 Qed.
 Hint Resolve Rplus_opp_l: real.
 
 
 (**********)
 Lemma Rplus_opp_r_uniq : forall r1 r2, r1 + r2 = 0 -> r2 = - r1.
-  intros x y H; replace y with (- x + x + y);
-   [ rewrite Rplus_assoc; rewrite H; ring | ring ].
+  intros x y H;
+  replace y with (- x + x + y) by ring.
+  rewrite Rplus_assoc; rewrite H; ring.
 Qed.
 
 (*i New i*)
@@ -311,16 +392,16 @@ Qed.
 
 (**********)
 Lemma Rinv_r : forall r, r <> 0 -> r * / r = 1.
-  intros; rewrite Rmult_comm; auto with real.
+  intros; field; trivial.
 Qed.
 Hint Resolve Rinv_r: real.
 
 Lemma Rinv_l_sym : forall r, r <> 0 -> 1 = / r * r.
-  symmetry  in |- *; auto with real.
+  intros; field; trivial.
 Qed.
 
 Lemma Rinv_r_sym : forall r, r <> 0 -> 1 = r * / r.
-  symmetry  in |- *; auto with real.
+  intros; field; trivial.
 Qed.
 Hint Resolve Rinv_l_sym Rinv_r_sym: real.
 
@@ -359,10 +440,10 @@ Qed.
 (**********)
 Lemma Rmult_eq_reg_l : forall r r1 r2, r * r1 = r * r2 -> r <> 0 -> r1 = r2.
   intros; transitivity (/ r * r * r1).
-  rewrite Rinv_l; auto with real.
+  field; trivial.
   transitivity (/ r * r * r2).
   repeat rewrite Rmult_assoc; rewrite H; trivial.
-  rewrite Rinv_l; auto with real.
+  field; trivial.
 Qed.
 
 (**********)
@@ -481,7 +562,7 @@ Qed.
 Hint Resolve Rmult_opp_opp: real.
 
 Lemma Ropp_mult_distr_r_reverse : forall r1 r2, r1 * - r2 = - (r1 * r2).
-intros; rewrite <- Ropp_mult_distr_l_reverse; ring.
+intros; ring.
 Qed.
 
 (** Substraction *)
@@ -557,7 +638,7 @@ Qed.
 
 (** Inverse *)
 Lemma Rinv_1 : / 1 = 1.
-field; auto with real.
+field.
 Qed.
 Hint Resolve Rinv_1: real.
 
@@ -570,19 +651,19 @@ Hint Resolve Rinv_neq_0_compat: real.
 
 (*********)
 Lemma Rinv_involutive : forall r, r <> 0 -> / / r = r.
-intros; field; auto with real.
+intros; field; trivial.
 Qed.
 Hint Resolve Rinv_involutive: real.
 
 (*********)
 Lemma Rinv_mult_distr :
  forall r1 r2, r1 <> 0 -> r2 <> 0 -> / (r1 * r2) = / r1 * / r2.
-intros; field; auto with real.
+intros; field; auto.
 Qed.
 
 (*********)
 Lemma Ropp_inv_permute : forall r, r <> 0 -> - / r = / - r.
-intros; field; auto with real.
+intros; field; trivial.
 Qed.
 
 Lemma Rinv_r_simpl_r : forall r1 r2, r1 <> 0 -> r1 * / r1 * r2 = r2.
@@ -1602,7 +1683,7 @@ intro H4;
 rewrite Rmult_1_r; replace (2 * x) with (x + x).
 rewrite (Rplus_comm y); intro H5; apply Rplus_le_reg_l with x; assumption.
 ring. 
-replace 2 with (INR 2); [ apply not_O_INR; discriminate | ring ].
+replace 2 with (INR 2); [ apply not_O_INR; discriminate | reflexivity ].
 pattern y at 2 in |- *; replace y with (y / 2 + y / 2).
 unfold Rminus, Rdiv in |- *.
 repeat rewrite Rmult_plus_distr_r.
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
index d6f796c42..5d35ad0dd 100644
--- a/theories/Reals/R_Ifp.v
+++ b/theories/Reals/R_Ifp.v
@@ -542,4 +542,4 @@ intros; unfold frac_part in |- *; generalize (plus_Int_part2 r1 r2 H); intro;
  rewrite <- (Rplus_assoc r1 r2 (- IZR (Int_part r1) + - IZR (Int_part r2)));
  rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2)));
  unfold Rminus in |- *; trivial with zarith real.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v
index f438ec863..a7118505b 100644
--- a/theories/Reals/Ranalysis.v
+++ b/theories/Reals/Ranalysis.v
@@ -797,6 +797,6 @@ Ltac reg :=
             [ simplify_derive aux X2;
                try
                 unfold plus_fct, minus_fct, mult_fct, div_fct, id, fct_cte,
-                 inv_fct, opp_fct in |- *; try ring
+                 inv_fct, opp_fct in |- *; (ring || ring_simplify)
             | try apply pr_nu ]) || is_diff_pt))
-  end.
\ No newline at end of file
+  end.
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index 248c8ce73..5a9ea513c 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -1114,7 +1114,7 @@ apply Ropp_gt_lt_contravar;
      Rmin (delta / 2) ((b + - c) / 2))) in |- *; apply Rplus_lt_le_0_compat;
  [ assumption
  | rewrite <- Ropp_0; apply Ropp_ge_le_contravar; apply Rle_ge; assumption ].
-ring.
+unfold Rminus; ring.
 rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; assumption.
 replace
  ((f (c + Rmin (delta / 2) ((b - c) / 2)) - f c) /
@@ -1306,10 +1306,7 @@ prove_sup0.
 replace (2 * (c + (a - c) / 2)) with (a + c).
 rewrite double.
 apply Rplus_lt_compat_l; assumption.
-ring.
-rewrite <- Rplus_assoc.
-rewrite <- double_var.
-ring.
+field; discrR.
 assumption.
 unfold Rabs in |- *; case (Rcase_abs (Rmax (- (delta / 2)) ((a - c) / 2))).
 intro; generalize (RmaxLess1 (- (delta / 2)) ((a - c) / 2)); intro;
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index 506853967..ab1c07474 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -11,4 +11,4 @@
 Require Export Rdefinitions.
 Require Export Raxioms.
 Require Export RIneq.
-Require Export DiscrR.
\ No newline at end of file
+Require Export DiscrR.
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 295c59ca1..878d5f73d 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -15,6 +15,8 @@
 (**          Definition of the sum functions            *)
 (*                                                      *)
 (********************************************************)
+Require Export ArithRing. (* for ring_nat... *)
+Require Export NewArithRing.
 
 Require Import Rbase.
 Require Export R_Ifp.
@@ -380,8 +382,7 @@ replace (2 * S n)%nat with (S (S (2 * n))).
 replace (x ^ S (S (2 * n))) with (x * x * x ^ (2 * n)).
 rewrite Hrecn; reflexivity.
 simpl in |- *; ring.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR;
- ring.
+ring_nat.
 Qed.
 
 Lemma pow_le : forall (a:R) (n:nat), 0 <= a -> 0 <= a ^ n.
@@ -429,7 +430,7 @@ do 2 rewrite pow_add.
 rewrite Hrecn2.
 simpl in |- *.
 ring.
-apply INR_eq; rewrite plus_INR; do 2 rewrite mult_INR; rewrite S_INR; ring.
+ring_nat.
 Qed.
 
 Lemma pow_incr : forall (x y:R) (n:nat), 0 <= x <= y -> x ^ n <= y ^ n.
@@ -747,7 +748,7 @@ Qed.
 (*********)
 Lemma R_dist_sym : forall x y:R, R_dist x y = R_dist y x.
 Proof.
-unfold R_dist in |- *; intros; split_Rabs; ring.
+unfold R_dist in |- *; intros; split_Rabs; try ring.
 generalize (Ropp_gt_lt_0_contravar (y - x) r); intro;
  rewrite (Ropp_minus_distr y x) in H; generalize (Rlt_asym (x - y) 0 r0);
  intro; unfold Rgt in H; elimtype False; auto.
diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v
index e7858a18f..5e953d94c 100644
--- a/theories/Reals/Rgeom.v
+++ b/theories/Reals/Rgeom.v
@@ -146,7 +146,7 @@ intros; unfold xr, yr in |- *;
     (- x1 * sin theta + y1 * cos theta - (- x2 * sin theta + y2 * cos theta))
     with (cos theta * (y1 - y2) + sin theta * (x2 - x1));
     [ repeat rewrite Rsqr_plus; repeat rewrite Rsqr_mult; repeat rewrite cos2;
-       ring; replace (x2 - x1) with (- (x1 - x2));
+       ring_simplify; replace (x2 - x1) with (- (x1 - x2));
        [ rewrite <- Rsqr_neg; ring | ring ]
     | ring ]
  | ring ].
@@ -184,4 +184,4 @@ Lemma isometric_trans_rot :
    Rsqr (xt (xr x1 y1 theta) tx - xt (xr x2 y2 theta) tx) +
    Rsqr (yt (yr x1 y1 theta) ty - yt (yr x2 y2 theta) ty). 
 intros; rewrite <- isometric_translation; apply isometric_rotation_0.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index d850d7f89..2bab67b8e 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -323,7 +323,7 @@ apply Ropp_lt_cancel.
 apply Rplus_lt_reg_r with (r := y).
 replace (y + - (y * exp (- eps))) with (y * (1 - exp (- eps)));
  [ idtac | ring ].
-replace (y + - x) with (Rabs (x - y)); [ idtac | ring ].
+replace (y + - x) with (Rabs (x - y)).
 apply Rlt_le_trans with (1 := H5); apply Rmin_r.
 rewrite Rabs_left; [ ring | idtac ].
 apply (Rlt_minus _ _ Hxy).
@@ -345,7 +345,7 @@ apply H.
 rewrite Hxyy.
 apply Rplus_lt_reg_r with (r := - y).
 replace (- y + y * exp eps) with (y * (exp eps - 1)); [ idtac | ring ].
-replace (- y + x) with (Rabs (x - y)); [ idtac | ring ].
+replace (- y + x) with (Rabs (x - y)).
 apply Rlt_le_trans with (1 := H5); apply Rmin_l.
 rewrite Rabs_right; [ ring | idtac ].
 left; apply (Rgt_minus _ _ Hxy).
@@ -619,7 +619,7 @@ intros x H0; repeat split.
 assumption.
 apply D_in_ext with (f := fun x:R => / x * (z * exp (z * ln x))).
 unfold Rminus in |- *; rewrite Rpower_plus; rewrite Rpower_Ropp;
- rewrite (Rpower_1 _ H); ring.
+ rewrite (Rpower_1 _ H); unfold Rpower; ring.
 apply Dcomp with
  (f := ln)
  (g := fun x:R => exp (z * x))
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v
index b29fb6a98..09f3eb5d2 100644
--- a/theories/Reals/Rprod.v
+++ b/theories/Reals/Rprod.v
@@ -38,13 +38,9 @@ rewrite H1; simpl in |- *; rewrite <- minus_n_n; simpl in |- *; ring.
 replace (S n - k)%nat with (S (n - k)).
 simpl in |- *; replace (k + S (n - k))%nat with (S n).
 rewrite Hrecn; [ ring | assumption ].
-apply INR_eq; rewrite S_INR; rewrite plus_INR; rewrite S_INR;
- rewrite minus_INR; [ ring | assumption ].
-apply INR_eq; rewrite S_INR; repeat rewrite minus_INR.
-rewrite S_INR; ring.
-apply le_trans with n; [ assumption | apply le_n_Sn ].
-assumption.
-inversion H; [ left; reflexivity | right; assumption ].
+omega.
+omega.
+omega.
 Qed.
 
 (**********)
@@ -116,18 +112,8 @@ apply prod_SO_Rle; intros; split.
 apply pos_INR.
 apply le_INR; apply plus_le_compat_r; assumption.
 assumption.
-apply INR_eq; repeat rewrite minus_INR.
-rewrite mult_INR; repeat rewrite S_INR; ring.
-apply le_trans with N; [ assumption | apply le_n_2n ].
-apply (fun p n m:nat => plus_le_reg_l n m p) with k; rewrite <- le_plus_minus.
-replace (2 * N)%nat with (N + N)%nat; [ idtac | ring ].
-apply plus_le_compat_r; assumption.
-assumption.
-assumption.
-apply (fun p n m:nat => plus_le_reg_l n m p) with k; rewrite <- le_plus_minus.
-replace (2 * N)%nat with (N + N)%nat; [ idtac | ring ].
-apply plus_le_compat_r; assumption.
-assumption.
+omega.
+omega.
 rewrite <- (Rmult_comm (prod_f_SO (fun l:nat => INR l) k));
  rewrite (prod_SO_split (fun l:nat => INR l) k N).
 rewrite Rmult_assoc; apply Rmult_le_compat_l.
@@ -140,24 +126,11 @@ replace (N - (2 * N - k))%nat with (k - N)%nat.
 apply prod_SO_Rle; intros; split.
 apply pos_INR.
 apply le_INR; apply plus_le_compat_r.
-apply (fun p n m:nat => plus_le_reg_l n m p) with k; rewrite <- le_plus_minus.
-replace (2 * N)%nat with (N + N)%nat; [ idtac | ring ];
- apply plus_le_compat_r; assumption.
-assumption.
-apply INR_eq; repeat rewrite minus_INR.
-rewrite mult_INR; do 2 rewrite S_INR; ring.
-assumption.
-apply (fun p n m:nat => plus_le_reg_l n m p) with k; rewrite <- le_plus_minus.
-replace (2 * N)%nat with (N + N)%nat; [ idtac | ring ];
- apply plus_le_compat_r; assumption.
-assumption.
-assumption.
-apply (fun p n m:nat => plus_le_reg_l n m p) with k; rewrite <- le_plus_minus.
-replace (2 * N)%nat with (N + N)%nat; [ idtac | ring ];
- apply plus_le_compat_r; assumption.
-assumption.
+omega.
+omega.
+omega.
 assumption.
-elim (le_dec k N); intro; [ left; assumption | right; assumption ].
+omega.
 Qed.
 
 (**********)
@@ -186,6 +159,5 @@ assumption.
 reflexivity.
 rewrite mult_INR; apply prod_neq_R0; apply INR_fact_neq_0.
 apply prod_neq_R0; apply INR_fact_neq_0.
-apply INR_eq; rewrite minus_INR;
- [ rewrite mult_INR; do 2 rewrite S_INR; ring | apply le_n_2n ].
+omega.
 Qed.
diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
index ee2d7c55d..319701ca1 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.v
@@ -52,21 +52,15 @@ apply (decomp_sum (fun i:nat => f (S k + i))).
 apply lt_minus_O_lt; assumption.
 apply sum_eq; intros; replace (S k + S i)%nat with (S (S k) + i)%nat.
 reflexivity.
-apply INR_eq; do 2 rewrite plus_INR; do 3 rewrite S_INR; ring.
+ring_nat.
 replace (high - S (S k))%nat with (high - S k - 1)%nat.
 apply pred_of_minus.
-apply INR_eq; repeat rewrite minus_INR.
-do 4 rewrite S_INR; ring.
-apply lt_le_S; assumption.
-apply lt_le_weak; assumption.
-apply lt_le_S; apply lt_minus_O_lt; assumption.
+omega.
 unfold sigma in |- *; replace (S k - low)%nat with (S (k - low)).
 pattern (S k) at 1 in |- *; replace (S k) with (low + S (k - low))%nat.
 symmetry  in |- *; apply (tech5 (fun i:nat => f (low + i))).
-apply INR_eq; rewrite plus_INR; do 2 rewrite S_INR; rewrite minus_INR.
-ring.
-assumption.
-apply minus_Sn_m; assumption.
+omega.
+omega.
 rewrite <- H2; unfold sigma in |- *; rewrite <- minus_n_n; simpl in |- *;
  replace (high - S low)%nat with (pred (high - low)).
 replace (sum_f_R0 (fun k0:nat => f (S (low + k0))) (pred (high - low))) with
@@ -76,14 +70,8 @@ apply lt_minus_O_lt.
 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.
-apply INR_eq; rewrite plus_INR; do 2 rewrite S_INR; rewrite plus_INR; ring.
-replace (high - S low)%nat with (high - low - 1)%nat.
-apply pred_of_minus.
-apply INR_eq; repeat rewrite minus_INR.
-do 2 rewrite S_INR; ring.
-apply lt_le_S; rewrite H2; assumption.
-rewrite H2; apply lt_le_weak; assumption.
-apply lt_le_S; apply lt_minus_O_lt; rewrite H2; assumption.
+ring_nat.
+omega.
 inversion H; [ right; reflexivity | left; assumption ].
 Qed.
 
@@ -137,4 +125,4 @@ intro; unfold sigma in |- *; rewrite <- minus_n_n.
 simpl in |- *; replace (low + 0)%nat with low; [ reflexivity | ring ].
 Qed.
 
-End Sigma.
\ No newline at end of file
+End Sigma.
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index f8db0463f..7f6b59b35 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -251,18 +251,24 @@ Qed.
 
 Lemma sin_period : forall (x:R) (k:nat), sin (x + 2 * INR k * PI) = sin x.
 intros x k; induction  k as [| k Hreck].
-cut (x + 2 * INR 0 * PI = x); [ intro; rewrite H; reflexivity | ring ].
-replace (x + 2 * INR (S k) * PI) with (x + 2 * INR k * PI + 2 * PI);
- [ rewrite sin_plus; rewrite sin_2PI; rewrite cos_2PI; ring; apply Hreck
- | rewrite S_INR; ring ].
+simpl in |- *;  ring_simplify (x + 2 * 0 * PI).
+trivial.
+
+replace (x + 2 * INR (S k) * PI) with (x + 2 * INR k * PI + 2 * PI).
+rewrite sin_plus in |- *; rewrite sin_2PI in |- *; rewrite cos_2PI in |- *.
+ring_simplify; trivial.
+rewrite S_INR in |- *;  ring.
 Qed.
 
 Lemma cos_period : forall (x:R) (k:nat), cos (x + 2 * INR k * PI) = cos x.
 intros x k; induction  k as [| k Hreck].
-cut (x + 2 * INR 0 * PI = x); [ intro; rewrite H; reflexivity | ring ].
-replace (x + 2 * INR (S k) * PI) with (x + 2 * INR k * PI + 2 * PI);
- [ rewrite cos_plus; rewrite sin_2PI; rewrite cos_2PI; ring; apply Hreck
- | rewrite S_INR; ring ].
+simpl in |- *;  ring_simplify (x + 2 * 0 * PI).
+trivial.
+
+replace (x + 2 * INR (S k) * PI) with (x + 2 * INR k * PI + 2 * PI).
+rewrite cos_plus in |- *; rewrite sin_2PI in |- *; rewrite cos_2PI in |- *.
+ring_simplify; trivial.
+rewrite S_INR in |- *;  ring.
 Qed.
 
 Lemma sin_shift : forall x:R, sin (PI / 2 - x) = cos x.
@@ -421,12 +427,10 @@ intro; apply Rplus_le_le_0_compat; repeat apply Rmult_le_pos;
 unfold x in |- *; replace 0 with (INR 0);
  [ apply le_INR; apply le_O_n | reflexivity ].
 prove_sup0.
-apply INR_eq; do 2 rewrite S_INR; do 3 rewrite plus_INR; rewrite mult_INR;
- repeat rewrite S_INR; ring.
+ring_nat.
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
-apply INR_eq; do 3 rewrite plus_INR; do 2 rewrite mult_INR;
- repeat rewrite S_INR; ring.
+ring_nat.
 Qed.
 
 Lemma SIN : forall a:R, 0 <= a -> a <= PI -> sin_lb a <= sin a <= sin_ub a.
@@ -1494,9 +1498,10 @@ Lemma cos_eq_0_0 :
  forall x:R, cos x = 0 ->  exists k : Z, x = IZR k * PI + PI / 2. 
 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; ring; rewrite Rmult_comm; rewrite <- H3;
- unfold INR in |- *.
-rewrite (double_var (- PI)); unfold Rdiv in |- *; ring.
+ rewrite <- Z_R_minus; simpl; ring_simplify;
+(* rewrite (Rmult_comm PI);*) (* old ring compat *)
+ rewrite <- H3; simpl;
+ 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 7a4921628..f74b2763c 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -119,8 +119,7 @@ replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
 simpl in |- *; ring.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite plus_INR;
- do 2 rewrite mult_INR; repeat rewrite S_INR; ring.
+ring_nat.
 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.
@@ -133,7 +132,7 @@ apply le_n_2n.
 apply (fun m n p:nat => mult_le_compat_l p n m); apply le_n_Sn.
 apply (fun m n p:nat => mult_le_compat_l p n m); apply le_n_S; assumption.
 apply le_n_Sn.
-apply INR_eq; rewrite S_INR; rewrite plus_INR; rewrite mult_INR; reflexivity.
+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;
@@ -201,12 +200,10 @@ unfold Rdiv in |- *; ring.
 reflexivity.
 replace (2 * (n + 1))%nat with (S (S (2 * n))).
 reflexivity.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; rewrite plus_INR;
- repeat rewrite S_INR; ring.
+ring.
 replace (2 * n + 1)%nat with (S (2 * n)).
 reflexivity.
-apply INR_eq; rewrite S_INR; rewrite plus_INR; rewrite mult_INR;
- repeat rewrite S_INR; ring.
+ring.
 intro; elim H1; intros.
 split.
 apply Rplus_le_reg_l with (- a).
@@ -219,12 +216,10 @@ unfold sin_term in |- *; simpl in |- *; unfold Rdiv in |- *; rewrite Rinv_1;
  ring.
 replace (2 * (n + 1))%nat with (S (S (2 * n))).
 apply lt_O_Sn.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; rewrite plus_INR;
- repeat rewrite S_INR; ring.
+ring.
 replace (2 * n + 1)%nat with (S (2 * n)).
 apply lt_O_Sn.
-apply INR_eq; rewrite S_INR; rewrite plus_INR; rewrite mult_INR;
- repeat rewrite S_INR; ring.
+ring.
 inversion H; [ assumption | elim Hyp_a; symmetry  in |- *; assumption ].
 Qed.
 
@@ -318,8 +313,7 @@ replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
 simpl in |- *; ring.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR;
- ring.
+ring_nat.
 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.
@@ -385,12 +379,10 @@ unfold Rdiv in |- *; ring.
 reflexivity.
 replace (2 * (n0 + 1))%nat with (S (S (2 * n0))).
 reflexivity.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; rewrite plus_INR;
- repeat rewrite S_INR; ring.
+ring.
 replace (2 * n0 + 1)%nat with (S (2 * n0)).
 reflexivity.
-apply INR_eq; rewrite S_INR; rewrite plus_INR; rewrite mult_INR;
- repeat rewrite S_INR; ring.
+ring.
 intro; elim H2; intros; split.
 apply Rplus_le_reg_l with (-1).
 rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l;
@@ -402,12 +394,10 @@ unfold cos_term in |- *; simpl in |- *; unfold Rdiv in |- *; rewrite Rinv_1;
  ring.
 replace (2 * (n0 + 1))%nat with (S (S (2 * n0))).
 apply lt_O_Sn.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; rewrite plus_INR;
- repeat rewrite S_INR; ring.
+ring.
 replace (2 * n0 + 1)%nat with (S (2 * n0)).
 apply lt_O_Sn.
-apply INR_eq; rewrite S_INR; rewrite plus_INR; rewrite mult_INR;
- repeat rewrite S_INR; ring.
+ring.
 intros; case (total_order_T 0 a); intro.
 elim s; intro.
 apply H; [ left; assumption | assumption ].
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index d9e96b9c5..88ddbccc1 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -98,8 +98,7 @@ unfold Rsqr in |- *; ring.
 apply pow_nonzero; assumption.
 replace (2 * S n)%nat with (S (S (2 * n))).
 simpl in |- *; ring.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR;
- ring.
+ring_nat.
 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.
@@ -277,8 +276,7 @@ unfold Rsqr in |- *; ring.
 apply pow_nonzero; assumption.
 replace (2 * S n)%nat with (S (S (2 * n))).
 simpl in |- *; ring.
-apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR;
- ring.
+ring_nat.
 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 484e0f217..06e6771f8 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -1228,8 +1228,8 @@ apply plus_lt_compat_r.
 apply lt_le_trans with 1%nat; [ apply lt_O_Sn | assumption ].
 apply INR_fact_neq_0.
 apply not_O_INR; discriminate.
-apply INR_eq; rewrite S_INR; do 3 rewrite plus_INR; reflexivity.
-apply INR_eq; do 3 rewrite plus_INR; do 2 rewrite S_INR; ring.
+ring_nat.
+ring_nat.
 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.
@@ -1253,12 +1253,11 @@ rewrite fact_simpl; rewrite mult_INR; rewrite Rmult_assoc;
 rewrite Rmult_1_r; apply Rle_trans with (INR M_nat).
 left; rewrite INR_IZR_INZ.
 rewrite <- H4; assert (H8 := archimed (Rabs x)); elim H8; intros; assumption.
-apply le_INR; apply le_trans with (S M_nat);
- [ apply le_n_Sn | apply le_n_S; apply le_plus_l ].
+apply le_INR; omega.
 apply INR_fact_neq_0.
 apply INR_fact_neq_0.
-apply INR_eq; rewrite S_INR; do 3 rewrite plus_INR; reflexivity.
-apply INR_eq; do 3 rewrite plus_INR; do 2 rewrite S_INR; ring.
+ring_nat.
+ring_nat.
 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;
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 884f05e52..b56818629 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -82,7 +82,7 @@ Lemma about_carrier_of_relation_class_and_relation_class_of_argument_class :
 
 Inductive nelistT (A : Type) : Type :=
    singl : A -> nelistT A
- | cons : A -> nelistT A -> nelistT A.
+ | necons : A -> nelistT A -> nelistT A.
 
 Definition Arguments := nelistT Argument_Class.
 
@@ -132,7 +132,7 @@ Record Morphism_Theory In Out : Type :=
 Definition list_of_Leibniz_of_list_of_types: nelistT Type -> Arguments.
  induction 1.
    exact (singl (Leibniz _ a)).
-   exact (cons (Leibniz _ a) IHX).
+   exact (necons (Leibniz _ a) IHX).
 Defined.
 
 (* every function is a morphism from Leibniz+ to Leibniz *)
@@ -175,7 +175,7 @@ Defined.
 Definition equality_morphism_of_symmetric_areflexive_transitive_relation:
  forall (A: Type)(Aeq: relation A)(sym: symmetric _ Aeq)(trans: transitive _ Aeq),
   let ASetoidClass := SymmetricAreflexive _ sym in
-   (Morphism_Theory (cons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class).
+   (Morphism_Theory (necons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class).
  intros.
  exists Aeq.
  unfold make_compatibility_goal; simpl; split; eauto.
@@ -184,7 +184,7 @@ Defined.
 Definition equality_morphism_of_symmetric_reflexive_transitive_relation:
  forall (A: Type)(Aeq: relation A)(refl: reflexive _ Aeq)(sym: symmetric _ Aeq)
   (trans: transitive _ Aeq), let ASetoidClass := SymmetricReflexive _ sym refl in
-   (Morphism_Theory (cons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class).
+   (Morphism_Theory (necons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class).
  intros.
  exists Aeq.
  unfold make_compatibility_goal; simpl; split; eauto.
@@ -194,7 +194,7 @@ Definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
  forall (A: Type)(Aeq: relation A)(trans: transitive _ Aeq),
   let ASetoidClass1 := AsymmetricAreflexive Contravariant Aeq in
   let ASetoidClass2 := AsymmetricAreflexive Covariant Aeq in
-   (Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
+   (Morphism_Theory (necons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
  intros.
  exists Aeq.
  unfold make_compatibility_goal; simpl; unfold impl; eauto.
@@ -204,7 +204,7 @@ Definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
  forall (A: Type)(Aeq: relation A)(refl: reflexive _ Aeq)(trans: transitive _ Aeq),
   let ASetoidClass1 := AsymmetricReflexive Contravariant refl in
   let ASetoidClass2 := AsymmetricReflexive Covariant refl in
-   (Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
+   (Morphism_Theory (necons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
  intros.
  exists Aeq.
  unfold make_compatibility_goal; simpl; unfold impl; eauto.
@@ -331,7 +331,7 @@ with Morphism_Context_List Hole dir :
        check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' ->
         Morphism_Context Hole dir (relation_class_of_argument_class S) dir' ->
          Morphism_Context_List Hole dir dir'' L ->
-          Morphism_Context_List Hole dir dir'' (cons S L).
+          Morphism_Context_List Hole dir dir'' (necons S L).
 
 Scheme Morphism_Context_rect2 := Induction for Morphism_Context  Sort Type
 with Morphism_Context_List_rect2 := Induction for Morphism_Context_List Sort Type.
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index d3b8a37f0..718ac3b03 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -8,7 +8,8 @@
 
 (*i $Id$ i*)
 
-Require Import ZArithRing.
+Require Import NewZArithRing.
+
 Require Import ZArith_base.
 Require Import Omega.
 Require Import Wf_nat.
@@ -209,4 +210,4 @@ End Zlength_properties.
 
 Implicit Arguments Zlength_correct [A].
 Implicit Arguments Zlength_cons [A].
-Implicit Arguments Zlength_nil_inv [A].
\ No newline at end of file
+Implicit Arguments Zlength_nil_inv [A].
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 025e03d4a..52f85eada 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -22,7 +22,7 @@ Then only after proves the main required property.
 Require Export ZArith_base.
 Require Import Zbool.
 Require Import Omega.
-Require Import ZArithRing.
+Require Import NewZArithRing.
 Require Import Zcomplements.
 Open Local Scope Z_scope.
 
@@ -148,7 +148,7 @@ case (Zgt_bool b (2 * r)); rewrite BinInt.Zpos_xO;
  (split; [ ring | omega ]).
 
 generalize (Zge_cases b 2).
-case (Zge_bool b 2); (intros; split; [ ring | omega ]).
+case (Zge_bool b 2); (intros; split; [ try ring | omega ]).
 omega.
 Qed.
 
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 05076ebd3..14bfa6357 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -9,7 +9,7 @@
 (*i $Id$ i*)
 
 Require Import ZArith_base.
-Require Import ZArithRing.
+Require Import NewZArithRing.
 Require Import Zcomplements.
 Require Import Zdiv.
 Require Import Ndigits.
@@ -164,7 +164,7 @@ left; rewrite H0; rewrite e; ring.
 assert (Hqq0 : q0 * q = 1).
 apply Zmult_reg_l with a.
 assumption.
-ring.
+ring_simplify.
 pattern a at 2 in |- *; rewrite H2; ring.
 assert (q | 1).
 rewrite <- Hqq0; auto with zarith.
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index f61999362..3d57561ea 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -8,9 +8,9 @@
 
 (* $Id$ *)
 
+Require Import NewZArithRing.
 Require Import Omega.
 Require Export ZArith_base.
-Require Export ZArithRing.
 Open Local Scope Z_scope.
 
 (**********************************************************************)
@@ -86,7 +86,7 @@ refine
             end
         end
     end); clear sqrtrempos; repeat compute_POS;
- try (try rewrite Heq; ring; fail); try omega.
+ try (try rewrite Heq; ring); try omega.
 Defined.
 
 (** Define with integer input, but with a strong (readable) specification. *)
@@ -132,7 +132,7 @@ refine
                (fun r:Z => 0 = 0 * 0 + r /\ 0 * 0 <= 0 < (0 + 1) * (0 + 1)) 0
                _)
     end); try omega.
-split; [ omega | rewrite Heq; ring ((s + 1) * (s + 1)); omega ].
+split; [ omega | rewrite Heq; ring_simplify ((s + 1) * (s + 1)); omega ].
 Defined.
 
 (** Define a function of type Z->Z that computes the integer square root,