ZArith + other : favor the use of modern names instead of compat notations

 - For instance, refl_equal --> eq_refl
 - Npos, Zpos, Zneg now admit more uniform qualified aliases
   N.pos, Z.pos, Z.neg.
 - A new module BinInt.Pos2Z with results about injections from
   positive to Z
 - A result about Z.pow pushed in the generic layer
 - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
 - Using tactic Z.le_elim instead of Zle_lt_or_eq
 - Some cleanup in ring, field, micromega
   (use of "Equivalence", "Proper" ...)
 - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
 - In ZMake and ZMake, functor parameters are now named NN and ZZ
   instead of N and Z for avoiding confusions

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

22 files changed, 145 insertions, 149 deletions

diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index 648055d93..87f1aaf72 100644
--- a/theories/Reals/AltSeries.v
+++ b/theories/Reals/AltSeries.v
@@ -374,7 +374,7 @@ Proof.
     replace (/ (2 * eps) * (INR N * (2 * eps))) with
       (INR N * (2 * eps * / (2 * eps))); [ idtac | ring ].
   rewrite <- Rinv_r_sym.
-  rewrite Rmult_1_r; replace (INR N) with (IZR (Z_of_nat N)).
+  rewrite Rmult_1_r; replace (INR N) with (IZR (Z.of_nat N)).
   rewrite <- H4.
   elim H1; intros; assumption.
   symmetry  in |- *; apply INR_IZR_INZ.
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index 2a828a90a..9a38888da 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -770,7 +770,7 @@ Proof.
   split.
   unfold D_x, no_cond in |- *; split.
   trivial.
-  apply (sym_not_eq H6).
+  apply (not_eq_sym H6).
   rewrite Rminus_0_r; apply H7.
   unfold SFL in |- *.
   case (cv 0); intros.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 7cf372e63..2f58201f7 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -58,7 +58,7 @@ Qed.
 
 Lemma Rgt_not_eq : forall r1 r2, r1 > r2 -> r1 <> r2.
 Proof.
-  intros; apply sym_not_eq; apply Rlt_not_eq; auto with real.
+  intros; apply not_eq_sym; apply Rlt_not_eq; auto with real.
 Qed.
 
 (**********)
@@ -278,8 +278,8 @@ Proof. intros; red; apply Rlt_eq_compat with (r2:=r4) (r4:=r2); auto. Qed.
 
 Lemma Rle_trans : forall r1 r2 r3, r1 <= r2 -> r2 <= r3 -> r1 <= r3.
 Proof.
-  generalize trans_eq Rlt_trans Rlt_eq_compat.
-  unfold Rle in |- *.
+  generalize eq_trans Rlt_trans Rlt_eq_compat.
+  unfold Rle.
   intuition eauto 2.
 Qed.
 
@@ -1389,7 +1389,7 @@ Qed.
 (**********)
 Lemma tech_Rplus : forall r (s:R), 0 <= r -> 0 < s -> r + s <> 0.
 Proof.
-  intros; apply sym_not_eq; apply Rlt_not_eq.
+  intros; apply not_eq_sym; apply Rlt_not_eq.
   rewrite Rplus_comm; replace 0 with (0 + 0); auto with real.
 Qed.
 Hint Immediate tech_Rplus: real.
@@ -1599,11 +1599,11 @@ Qed.
 Hint Resolve lt_1_INR: real.
 
 (**********)
-Lemma pos_INR_nat_of_P : forall p:positive, 0 < INR (nat_of_P p).
+Lemma pos_INR_nat_of_P : forall p:positive, 0 < INR (Pos.to_nat p).
 Proof.
   intro; apply lt_0_INR.
   simpl in |- *; auto with real.
-  apply nat_of_P_pos.
+  apply Pos2Nat.is_pos.
 Qed.
 Hint Resolve pos_INR_nat_of_P: real.
 
@@ -1666,7 +1666,7 @@ Proof.
   case (le_lt_or_eq _ _ H1); intros H2.
   apply Rlt_dichotomy_converse; auto with real.
   exfalso; auto.
-  apply sym_not_eq; apply Rlt_dichotomy_converse; auto with real.
+  apply not_eq_sym; apply Rlt_dichotomy_converse; auto with real.
 Qed.
 Hint Resolve not_INR: real.
 
@@ -1703,16 +1703,16 @@ Hint Resolve not_1_INR: real.
 
 
 (**********)
-Lemma IZN : forall n:Z, (0 <= n)%Z ->  exists m : nat, n = Z_of_nat m.
+Lemma IZN : forall n:Z, (0 <= n)%Z ->  exists m : nat, n = Z.of_nat m.
 Proof.
   intros z; idtac; apply Z_of_nat_complete; assumption.
 Qed.
 
 (**********)
-Lemma INR_IZR_INZ : forall n:nat, INR n = IZR (Z_of_nat n).
+Lemma INR_IZR_INZ : forall n:nat, INR n = IZR (Z.of_nat n).
 Proof.
   simple induction n; auto with real.
-  intros; simpl in |- *; rewrite nat_of_P_of_succ_nat;
+  intros; simpl in |- *; rewrite SuccNat2Pos.id_succ;
     auto with real.
 Qed.
 
@@ -1720,13 +1720,13 @@ Lemma plus_IZR_NEG_POS :
   forall p q:positive, IZR (Zpos p + Zneg q) = IZR (Zpos p) + IZR (Zneg q).
 Proof.
   intros p q; simpl. rewrite Z.pos_sub_spec.
-  case Pcompare_spec; intros H; simpl.
+  case Pos.compare_spec; intros H; simpl.
   subst. ring.
-  rewrite Pminus_minus by trivial.
-  rewrite minus_INR by (now apply lt_le_weak, Plt_lt).
+  rewrite Pos2Nat.inj_sub by trivial.
+  rewrite minus_INR by (now apply lt_le_weak, Pos2Nat.inj_lt).
   ring.
-  rewrite Pminus_minus by trivial.
-  rewrite minus_INR by (now apply lt_le_weak, Plt_lt).
+  rewrite Pos2Nat.inj_sub by trivial.
+  rewrite minus_INR by (now apply lt_le_weak, Pos2Nat.inj_lt).
   ring.
 Qed.
 
@@ -1734,10 +1734,10 @@ Qed.
 Lemma plus_IZR : forall n m:Z, IZR (n + m) = IZR n + IZR m.
 Proof.
   intro z; destruct z; intro t; destruct t; intros; auto with real.
-  simpl; intros; rewrite Pplus_plus; auto with real.
+  simpl; intros; rewrite Pos2Nat.inj_add; auto with real.
   apply plus_IZR_NEG_POS.
-  rewrite Zplus_comm; rewrite Rplus_comm; apply plus_IZR_NEG_POS.
-  simpl; intros; rewrite Pplus_plus; rewrite plus_INR;
+  rewrite Z.add_comm; rewrite Rplus_comm; apply plus_IZR_NEG_POS.
+  simpl; intros; rewrite Pos2Nat.inj_add; rewrite plus_INR;
     auto with real.
 Qed.
 
@@ -1745,31 +1745,31 @@ Qed.
 Lemma mult_IZR : forall n m:Z, IZR (n * m) = IZR n * IZR m.
 Proof.
   intros z t; case z; case t; simpl in |- *; auto with real.
-  intros t1 z1; rewrite Pmult_mult; auto with real.
-  intros t1 z1; rewrite Pmult_mult; auto with real.
+  intros t1 z1; rewrite Pos2Nat.inj_mul; auto with real.
+  intros t1 z1; rewrite Pos2Nat.inj_mul; auto with real.
   rewrite Rmult_comm.
   rewrite Ropp_mult_distr_l_reverse; auto with real.
   apply Ropp_eq_compat; rewrite mult_comm; auto with real.
-  intros t1 z1; rewrite Pmult_mult; auto with real.
+  intros t1 z1; rewrite Pos2Nat.inj_mul; auto with real.
   rewrite Ropp_mult_distr_l_reverse; auto with real.
-  intros t1 z1; rewrite Pmult_mult; auto with real.
+  intros t1 z1; rewrite Pos2Nat.inj_mul; auto with real.
   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)).
+Lemma pow_IZR : forall z n, pow (IZR z) n = IZR (Z.pow z (Z.of_nat n)).
 Proof.
  intros z [|n];simpl;trivial.
  rewrite Zpower_pos_nat.
- rewrite nat_of_P_of_succ_nat. unfold Zpower_nat;simpl.
+ rewrite SuccNat2Pos.id_succ. unfold Zpower_nat;simpl.
  rewrite mult_IZR.
  induction n;simpl;trivial.
  rewrite mult_IZR;ring[IHn].
 Qed.
 
 (**********)
-Lemma succ_IZR : forall n:Z, IZR (Zsucc n) = IZR n + 1.
+Lemma succ_IZR : forall n:Z, IZR (Z.succ n) = IZR n + 1.
 Proof.
-  intro; change 1 with (IZR 1); unfold Zsucc; apply plus_IZR.
+  intro; change 1 with (IZR 1); unfold Z.succ; apply plus_IZR.
 Qed.
 
 (**********)
@@ -1782,7 +1782,7 @@ Definition Ropp_Ropp_IZR := opp_IZR.
 
 Lemma minus_IZR : forall n m:Z, IZR (n - m) = IZR n - IZR m.
 Proof.
-  intros; unfold Zminus, Rminus.
+  intros; unfold Z.sub, Rminus.
   rewrite <- opp_IZR.
   apply plus_IZR.
 Qed.
@@ -1790,7 +1790,7 @@ Qed.
 (**********)
 Lemma Z_R_minus : forall n m:Z, IZR n - IZR m = IZR (n - m).
 Proof.
-  intros z1 z2; unfold Rminus in |- *; unfold Zminus in |- *.
+  intros z1 z2; unfold Rminus in |- *; unfold Z.sub in |- *.
   rewrite <- (Ropp_Ropp_IZR z2); symmetry  in |- *; apply plus_IZR.
 Qed.
 
@@ -1799,7 +1799,7 @@ Lemma lt_0_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z.
 Proof.
   intro z; case z; simpl in |- *; intros.
   absurd (0 < 0); auto with real.
-  unfold Zlt in |- *; simpl in |- *; trivial.
+  unfold Z.lt in |- *; simpl in |- *; trivial.
   case Rlt_not_le with (1 := H).
   replace 0 with (-0); auto with real.
 Qed.
@@ -1807,7 +1807,7 @@ Qed.
 (**********)
 Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z.
 Proof.
-  intros z1 z2 H; apply Zlt_0_minus_lt.
+  intros z1 z2 H; apply Z.lt_0_sub.
   apply lt_0_IZR.
   rewrite <- Z_R_minus.
   exact (Rgt_minus (IZR z2) (IZR z1) H).
@@ -1817,8 +1817,8 @@ Qed.
 Lemma eq_IZR_R0 : forall n:Z, IZR n = 0 -> n = 0%Z.
 Proof.
   intro z; destruct z; simpl in |- *; intros; auto with zarith.
-  case (Rlt_not_eq 0 (INR (nat_of_P p))); auto with real.
-  case (Rlt_not_eq (- INR (nat_of_P p)) 0); auto with real.
+  case (Rlt_not_eq 0 (INR (Pos.to_nat p))); auto with real.
+  case (Rlt_not_eq (- INR (Pos.to_nat p)) 0); auto with real.
   apply Ropp_lt_gt_0_contravar. unfold Rgt in |- *; apply pos_INR_nat_of_P.
 Qed.
 
@@ -1841,7 +1841,7 @@ Qed.
 Lemma le_0_IZR : forall n:Z, 0 <= IZR n -> (0 <= n)%Z.
 Proof.
   unfold Rle in |- *; intros z [H| H].
-  red in |- *; intro; apply (Zlt_le_weak 0 z (lt_0_IZR z H)); assumption.
+  red in |- *; intro; apply (Z.lt_le_incl 0 z (lt_0_IZR z H)); assumption.
   rewrite (eq_IZR_R0 z); auto with zarith real.
 Qed.
 
@@ -1849,7 +1849,7 @@ Qed.
 Lemma le_IZR : forall n m:Z, IZR n <= IZR m -> (n <= m)%Z.
 Proof.
   unfold Rle in |- *; intros z1 z2 [H| H].
-  apply (Zlt_le_weak z1 z2); auto with real.
+  apply (Z.lt_le_incl z1 z2); auto with real.
   apply lt_IZR; trivial.
   rewrite (eq_IZR z1 z2); auto with zarith real.
 Qed.
@@ -1885,10 +1885,10 @@ Qed.
 Lemma one_IZR_lt1 : forall n:Z, -1 < IZR n < 1 -> n = 0%Z.
 Proof.
   intros z [H1 H2].
-  apply Zle_antisym.
-  apply Zlt_succ_le; apply lt_IZR; trivial.
-  replace 0%Z with (Zsucc (-1)); trivial.
-  apply Zlt_le_succ; apply lt_IZR; trivial.
+  apply Z.le_antisymm.
+  apply Z.lt_succ_r; apply lt_IZR; trivial.
+  replace 0%Z with (Z.succ (-1)); trivial.
+  apply Z.le_succ_l; apply lt_IZR; trivial.
 Qed.
 
 Lemma one_IZR_r_R1 :
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
index 9e04a7daf..c089b648d 100644
--- a/theories/Reals/R_Ifp.v
+++ b/theories/Reals/R_Ifp.v
@@ -58,7 +58,7 @@ Proof.
       intros a b; rewrite b; clear a b; rewrite <- Z_R_minus;
         cut (up 0 = 1%Z).
   intro; rewrite H1;
-    rewrite (Rminus_diag_eq (IZR 1) (IZR 1) (refl_equal (IZR 1)));
+    rewrite (Rminus_diag_eq (IZR 1) (IZR 1) (eq_refl (IZR 1)));
       apply Ropp_0.
   elim (archimed 0); intros; clear H2; unfold Rgt in H1;
     rewrite (Rminus_0_r (IZR (up 0))) in H0; generalize (lt_O_IZR (up 0) H1);
@@ -130,16 +130,16 @@ Proof.
 Qed.
 
 (**********)
-Lemma Int_part_INR : forall n:nat, Int_part (INR n) = Z_of_nat n.
+Lemma Int_part_INR : forall n:nat, Int_part (INR n) = Z.of_nat n.
 Proof.
   intros n; unfold Int_part in |- *.
-  cut (up (INR n) = (Z_of_nat n + Z_of_nat 1)%Z).
+  cut (up (INR n) = (Z.of_nat n + Z.of_nat 1)%Z).
   intros H'; rewrite H'; simpl in |- *; ring.
-  apply sym_equal; apply tech_up; auto.
-  replace (Z_of_nat n + Z_of_nat 1)%Z with (Z_of_nat (S n)).
+  symmetry; apply tech_up; auto.
+  replace (Z.of_nat n + Z.of_nat 1)%Z with (Z.of_nat (S n)).
   repeat rewrite <- INR_IZR_INZ.
   apply lt_INR; auto.
-  rewrite Zplus_comm; rewrite <- Znat.inj_plus; simpl in |- *; auto.
+  rewrite Z.add_comm; rewrite <- Znat.Nat2Z.inj_add; simpl in |- *; auto.
   rewrite plus_IZR; simpl in |- *; auto with real.
   repeat rewrite <- INR_IZR_INZ; auto with real.
 Qed.
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v
index ed80ac433..732a61017 100644
--- a/theories/Reals/Ranalysis2.v
+++ b/theories/Reals/Ranalysis2.v
@@ -429,7 +429,7 @@ Proof.
     rewrite Rmult_1_r in H12; rewrite <- Rinv_r_sym in H12;
       [ idtac | discrR ].
   cut (IZR 1 < IZR 2).
-  unfold IZR in |- *; unfold INR, nat_of_P in |- *; simpl in |- *; intro;
+  unfold IZR in |- *; unfold INR, Pos.to_nat in |- *; simpl in |- *; intro;
     elim (Rlt_irrefl 1 (Rlt_trans _ _ _ H13 H12)).
   apply IZR_lt; omega.
   unfold Rabs in |- *; case (Rcase_abs (/ 2)); intro.
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 8f01d7d03..259e1ac04 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -122,8 +122,8 @@ Arguments INR n%nat.
 Definition IZR (z:Z) : R :=
   match z with
   | Z0 => 0
-  | Zpos n => INR (nat_of_P n)
-  | Zneg n => - INR (nat_of_P n)
+  | Zpos n => INR (Pos.to_nat n)
+  | Zneg n => - INR (Pos.to_nat n)
   end.
 Arguments IZR z%Z.
 
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 4bc7fd104..ee9ea921c 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -623,7 +623,7 @@ Proof.
   apply RmaxLess1; auto.
 Qed.
 
-Lemma Rabs_Zabs : forall z:Z, Rabs (IZR z) = IZR (Zabs z).
+Lemma Rabs_Zabs : forall z:Z, Rabs (IZR z) = IZR (Z.abs z).
 Proof.
   intros z; case z; simpl in |- *; auto with real.
   apply Rabs_right; auto with real.
@@ -632,7 +632,7 @@ Proof.
   apply Rabs_right; auto with real zarith.
 Qed.
 
-Lemma abs_IZR : forall z, IZR (Zabs z) = Rabs (IZR z).
+Lemma abs_IZR : forall z, IZR (Z.abs z) = Rabs (IZR z).
 Proof.
   intros.
   now rewrite Rabs_Zabs.
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v
index 105d8347d..8f9b99c28 100644
--- a/theories/Reals/Rderiv.v
+++ b/theories/Reals/Rderiv.v
@@ -85,7 +85,7 @@ Proof.
         unfold Rgt in |- *; intro; elim (H7 H5); clear H7;
           intros; clear H4 H5; generalize (H1 x1 (conj H3 H8));
             clear H1; intro; unfold D_x in H3; elim H3; intros;
-              generalize (sym_not_eq H5); clear H5; intro H5;
+              generalize (not_eq_sym H5); clear H5; intro H5;
                 generalize (Rminus_eq_contra x1 x0 H5); intro; generalize H1;
                   pattern (d x0) at 1 in |- *;
                     rewrite <- (let (H1, H2) := Rmult_ne (d x0) in H2);
@@ -177,8 +177,8 @@ Proof.
   unfold D_in in |- *; intros; unfold limit1_in in |- *;
     unfold limit_in in |- *; unfold Rdiv in |- *; intros;
       simpl in |- *; split with eps; split; auto.
-  intros; rewrite (Rminus_diag_eq y y (refl_equal y)); rewrite Rmult_0_l;
-    unfold R_dist in |- *; rewrite (Rminus_diag_eq 0 0 (refl_equal 0));
+  intros; rewrite (Rminus_diag_eq y y (eq_refl y)); rewrite Rmult_0_l;
+    unfold R_dist in |- *; rewrite (Rminus_diag_eq 0 0 (eq_refl 0));
       unfold Rabs in |- *; case (Rcase_abs 0); intro.
   absurd (0 < 0); auto.
   red in |- *; intro; apply (Rlt_irrefl 0 H1).
@@ -193,8 +193,8 @@ Proof.
     unfold limit_in in |- *; intros; simpl in |- *; split with eps;
       split; auto.
   intros; elim H0; clear H0; intros; unfold D_x in H0; elim H0; intros;
-    rewrite (Rinv_r (x - x0) (Rminus_eq_contra x x0 (sym_not_eq H3)));
-      unfold R_dist in |- *; rewrite (Rminus_diag_eq 1 1 (refl_equal 1));
+    rewrite (Rinv_r (x - x0) (Rminus_eq_contra x x0 (not_eq_sym H3)));
+      unfold R_dist in |- *; rewrite (Rminus_diag_eq 1 1 (eq_refl 1));
         unfold Rabs in |- *; case (Rcase_abs 0); intro.
   absurd (0 < 0); auto.
   red in |- *; intro; apply (Rlt_irrefl 0 r).
@@ -270,7 +270,7 @@ Proof.
   ring.
   unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; intros;
     split with eps; split; auto; intros; elim (R_dist_refl (g x0) (g x0));
-      intros a b; rewrite (b (refl_equal (g x0))); unfold Rgt in H;
+      intros a b; rewrite (b (eq_refl (g x0))); unfold Rgt in H;
         assumption.
 Qed.
 
@@ -391,7 +391,7 @@ Proof.
       rewrite (Rminus_diag_eq (f x2) (f x0) H12) in H16;
         rewrite (Rmult_0_l (/ (x2 - x0))) in H16;
           rewrite (Rmult_0_l (dg (f x0))) in H16; rewrite H12;
-            rewrite (Rminus_diag_eq (g (f x0)) (g (f x0)) (refl_equal (g (f x0))));
+            rewrite (Rminus_diag_eq (g (f x0)) (g (f x0)) (eq_refl (g (f x0))));
               rewrite (Rmult_0_l (/ (x2 - x0))); assumption.
   clear H10 H5; elim H11; clear H11; intros; elim H5; clear H5; intros;
     cut
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 5ba0a187c..4c4903cb2 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -25,8 +25,8 @@ Require Export SplitRmult.
 Require Export ArithProp.
 Require Import Omega.
 Require Import Zpower.
-Open Local Scope nat_scope.
-Open Local Scope R_scope.
+Local Open Scope nat_scope.
+Local Open Scope R_scope.
 
 (*******************************)
 (** * Lemmas about factorial   *)
@@ -221,8 +221,8 @@ Qed.
 Lemma RPow_abs : forall (x:R) (n:nat), Rabs x ^ n = Rabs (x ^ n).
 Proof.
   intro; simple induction n; simpl.
-  apply sym_eq; apply Rabs_pos_eq; apply Rlt_le; apply Rlt_0_1.
-  intros; rewrite H; apply sym_eq; apply Rabs_mult.
+  symmetry; apply Rabs_pos_eq; apply Rlt_le; apply Rlt_0_1.
+  intros; rewrite H; symmetry; apply Rabs_mult.
 Qed.
 
 
@@ -526,13 +526,13 @@ Qed.
 (*i Due to L.Thery i*)
 
 Ltac case_eq name :=
-  generalize (refl_equal name); pattern name at -1; case name.
+  generalize (eq_refl name); pattern name at -1; case name.
 
 Definition powerRZ (x:R) (n:Z) :=
   match n with
     | Z0 => 1
-    | Zpos p => x ^ nat_of_P p
-    | Zneg p => / x ^ nat_of_P p
+    | Zpos p => x ^ Pos.to_nat p
+    | Zneg p => / x ^ Pos.to_nat p
   end.
 
 Infix Local "^Z" := powerRZ (at level 30, right associativity) : R_scope.
@@ -548,7 +548,7 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma powerRZ_1 : forall x:R, x ^Z Zsucc 0 = x.
+Lemma powerRZ_1 : forall x:R, x ^Z Z.succ 0 = x.
 Proof.
   simpl; auto with real.
 Qed.
@@ -558,67 +558,63 @@ Proof.
   destruct z; simpl; auto with real.
 Qed.
 
+Lemma powerRZ_pos_sub (x:R) (n m:positive) : x <> 0 ->
+   x ^Z (Z.pos_sub n m) = x ^ Pos.to_nat n * / x ^ Pos.to_nat m.
+Proof.
+ intro Hx.
+ rewrite Z.pos_sub_spec.
+ case Pos.compare_spec; intro H; simpl.
+ - subst; auto with real.
+ - rewrite Pos2Nat.inj_sub by trivial.
+   rewrite Pos2Nat.inj_lt in H.
+   rewrite (pow_RN_plus x _ (Pos.to_nat n)) by auto with real.
+   rewrite plus_comm, le_plus_minus_r by auto with real.
+   rewrite Rinv_mult_distr, Rinv_involutive; auto with real.
+ - rewrite Pos2Nat.inj_sub by trivial.
+   rewrite Pos2Nat.inj_lt in H.
+   rewrite (pow_RN_plus x _ (Pos.to_nat m)) by auto with real.
+   rewrite plus_comm, le_plus_minus_r by auto with real.
+   reflexivity.
+Qed.
+
 Lemma powerRZ_add :
   forall (x:R) (n m:Z), x <> 0 -> x ^Z (n + m) = x ^Z n * x ^Z m.
 Proof.
-  intro x; destruct n as [| n1| n1]; destruct m as [| m1| m1]; simpl;
-    auto with real.
-(* POS/POS *)
-  rewrite Pplus_plus; auto with real.
-(* POS/NEG *)
-  rewrite Z.pos_sub_spec.
-  case Pcompare_spec; intros; simpl.
-  subst; auto with real.
-  rewrite Pminus_minus by trivial.
-  rewrite (pow_RN_plus x _ (nat_of_P n1)) by auto with real.
-  rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
-  rewrite Rinv_mult_distr, Rinv_involutive; auto with real.
-  rewrite Pminus_minus by trivial.
-  rewrite (pow_RN_plus x _ (nat_of_P m1)) by auto with real.
-  rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
-  reflexivity.
-(* NEG/POS *)
-  rewrite Z.pos_sub_spec.
-  case Pcompare_spec; intros; simpl.
-  subst; auto with real.
-  rewrite Pminus_minus by trivial.
-  rewrite (pow_RN_plus x _ (nat_of_P m1)) by auto with real.
-  rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
-  rewrite Rinv_mult_distr, Rinv_involutive; auto with real.
-  rewrite Pminus_minus by trivial.
-  rewrite (pow_RN_plus x _ (nat_of_P n1)) by auto with real.
-  rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
-  auto with real.
-(* NEG/NEG *)
-  rewrite Pplus_plus; auto with real.
-  intros H'; rewrite pow_add; auto with real.
-  apply Rinv_mult_distr; auto.
-  apply pow_nonzero; auto.
-  apply pow_nonzero; auto.
+  intros x [|n|n] [|m|m]; simpl; intros; auto with real.
+  - (* + + *)
+    rewrite Pos2Nat.inj_add; auto with real.
+  - (* + - *)
+    now apply powerRZ_pos_sub.
+  - (* - + *)
+    rewrite Rmult_comm. now apply powerRZ_pos_sub.
+  - (* - - *)
+    rewrite Pos2Nat.inj_add; auto with real.
+    rewrite pow_add; auto with real.
+    apply Rinv_mult_distr; apply pow_nonzero; auto.
 Qed.
 Hint Resolve powerRZ_O powerRZ_1 powerRZ_NOR powerRZ_add: real.
 
 Lemma Zpower_nat_powerRZ :
-  forall n m:nat, IZR (Zpower_nat (Z_of_nat n) m) = INR n ^Z Z_of_nat m.
+  forall n m:nat, IZR (Zpower_nat (Z.of_nat n) m) = INR n ^Z Z.of_nat m.
 Proof.
   intros n m; elim m; simpl; auto with real.
-  intros m1 H'; rewrite nat_of_P_of_succ_nat; simpl.
-  replace (Zpower_nat (Z_of_nat n) (S m1)) with
-  (Z_of_nat n * Zpower_nat (Z_of_nat n) m1)%Z.
+  intros m1 H'; rewrite SuccNat2Pos.id_succ; simpl.
+  replace (Zpower_nat (Z.of_nat n) (S m1)) with
+  (Z.of_nat n * Zpower_nat (Z.of_nat n) m1)%Z.
   rewrite mult_IZR; auto with real.
   repeat rewrite <- INR_IZR_INZ; simpl.
   rewrite H'; simpl.
   case m1; simpl; auto with real.
-  intros m2; rewrite nat_of_P_of_succ_nat; auto.
+  intros m2; rewrite SuccNat2Pos.id_succ; auto.
   unfold Zpower_nat; auto.
 Qed.
 
 Lemma Zpower_pos_powerRZ :
-  forall n m, IZR (Zpower_pos n m) = IZR n ^Z Zpos m.
+  forall n m, IZR (Z.pow_pos n m) = IZR n ^Z Zpos m.
 Proof.
   intros.
   rewrite Zpower_pos_nat; simpl.
-  induction (nat_of_P m).
+  induction (Pos.to_nat m).
   easy.
   unfold Zpower_nat; simpl.
   rewrite mult_IZR.
@@ -638,10 +634,10 @@ Qed.
 Hint Resolve powerRZ_le: real.
 
 Lemma Zpower_nat_powerRZ_absolu :
-  forall n m:Z, (0 <= m)%Z -> IZR (Zpower_nat n (Zabs_nat m)) = IZR n ^Z m.
+  forall n m:Z, (0 <= m)%Z -> IZR (Zpower_nat n (Z.abs_nat m)) = IZR n ^Z m.
 Proof.
   intros n m; case m; simpl; auto with zarith.
-  intros p H'; elim (nat_of_P p); simpl; auto with zarith.
+  intros p H'; elim (Pos.to_nat p); simpl; auto with zarith.
   intros n0 H'0; rewrite <- H'0; simpl; auto with zarith.
   rewrite <- mult_IZR; auto.
   intros p H'; absurd (0 <= Zneg p)%Z; auto with zarith.
@@ -650,9 +646,9 @@ Qed.
 Lemma powerRZ_R1 : forall n:Z, 1 ^Z n = 1.
 Proof.
   intros n; case n; simpl; auto.
-  intros p; elim (nat_of_P p); simpl; auto; intros n0 H'; rewrite H';
+  intros p; elim (Pos.to_nat p); simpl; auto; intros n0 H'; rewrite H';
     ring.
-  intros p; elim (nat_of_P p); simpl.
+  intros p; elim (Pos.to_nat p); simpl.
   exact Rinv_1.
   intros n1 H'; rewrite Rinv_mult_distr; try rewrite Rinv_1; try rewrite H';
     auto with real.
@@ -760,9 +756,9 @@ Qed.
 Lemma R_dist_refl : forall x y:R, R_dist x y = 0 <-> x = y.
 Proof.
   unfold R_dist; intros; split_Rabs; split; intros.
-  rewrite (Ropp_minus_distr x y) in H; apply sym_eq;
+  rewrite (Ropp_minus_distr x y) in H; symmetry;
     apply (Rminus_diag_uniq y x H).
-  rewrite (Ropp_minus_distr x y); generalize (sym_eq H); intro;
+  rewrite (Ropp_minus_distr x y); generalize (eq_sym H); intro;
     apply (Rminus_diag_eq y x H0).
   apply (Rminus_diag_uniq x y H).
   apply (Rminus_diag_eq x y H).
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index 013cbdce1..18c24c184 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -21,7 +21,7 @@ Set Implicit Arguments.
 Definition Nbound (I:nat -> Prop) : Prop :=
   exists n : nat, (forall i:nat, I i -> (i <= n)%nat).
 
-Lemma IZN_var : forall z:Z, (0 <= z)%Z -> {n : nat | z = Z_of_nat n}.
+Lemma IZN_var : forall z:Z, (0 <= z)%Z -> {n : nat | z = Z.of_nat n}.
 Proof.
   intros; apply Z_of_nat_complete_inf; assumption.
 Qed.
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 5c864de38..80b900af7 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -196,7 +196,7 @@ Proof.
   case (H0 (dist R_met (f x0) l)); auto.
   intros alpha1 [H2 H3]; apply H3; auto; split; auto.
   case (dist_refl R_met x0 x0); intros Hr1 Hr2; rewrite Hr2; auto.
-  case (dist_refl R_met (f x0) l); intros Hr1 Hr2; apply sym_eq; auto.
+  case (dist_refl R_met (f x0) l); intros Hr1 Hr2; symmetry; auto.
 Qed.
 
 (*********)
@@ -270,7 +270,7 @@ Lemma limit_free :
 Proof.
   unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; intros;
     split with eps; split; auto; intros; elim (R_dist_refl (f x) (f x));
-      intros a b; rewrite (b (refl_equal (f x))); unfold Rgt in H;
+      intros a b; rewrite (b (eq_refl (f x))); unfold Rgt in H;
         assumption.
 Qed.
 
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index 146e97361..b5bd2b734 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -561,7 +561,7 @@ Proof.
   apply Rminus_eq_contra.
   red in |- *; intros H2; case HD2.
   symmetry  in |- *; apply (ln_inv _ _ HD1 Hy H2).
-  apply Rminus_eq_contra; apply (sym_not_eq HD2).
+  apply Rminus_eq_contra; apply (not_eq_sym HD2).
   apply Rinv_neq_0_compat; apply Rminus_eq_contra; red in |- *; intros H2;
     case HD2; apply ln_inv; auto.
   assumption.
@@ -588,7 +588,7 @@ Proof.
     [ idtac | ring ].
   apply H1.
   elim H2; intros H3 _; unfold D_x in H3; elim H3; clear H3; intros _ H3;
-    apply Rminus_eq_contra; apply (sym_not_eq (A:=R));
+    apply Rminus_eq_contra; apply (not_eq_sym (A:=R));
       apply H3.
   elim H2; clear H2; intros _ H2; apply H2.
   assumption.
@@ -625,7 +625,7 @@ Proof.
   replace (- h - x / 2 + (x / 2 + x / 2 + h)) with (x / 2); [ apply H7 | ring ].
   apply r.
   apply Rplus_lt_le_0_compat; [ assumption | apply Rge_le; apply r ].
-  apply (sym_not_eq (A:=R)); apply Rminus_not_eq; replace (x + h - x) with h;
+  apply (not_eq_sym (A:=R)); apply Rminus_not_eq; replace (x + h - x) with h;
     [ apply H5 | ring ].
   replace (x + h - x) with h;
   [ apply Rlt_le_trans with alp;
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 479d381d4..9d1ba7381 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -182,13 +182,13 @@ Section sequence.
 
     assert (Hs0: forall n, sum n = 0).
     intros n.
-    specialize (Hm1 (sum n) (ex_intro _ _ (refl_equal _))).
+    specialize (Hm1 (sum n) (ex_intro _ _ (eq_refl _))).
     apply Rle_antisym with (2 := proj1 (Hsum n)).
     now rewrite <- Hm.
 
     assert (Hub: forall n, Un n <= l - eps).
     intros n.
-    generalize (refl_equal (sum (S n))).
+    generalize (eq_refl (sum (S n))).
     simpl sum at 1.
     rewrite 2!Hs0, Rplus_0_l.
     unfold test.
@@ -238,7 +238,7 @@ Section sequence.
     rewrite (IHN H6), Rplus_0_l.
     unfold test.
     destruct Rle_lt_dec.
-    apply refl_equal.
+    apply eq_refl.
     now elim Rlt_not_le with (1 := r).
 
     destruct (le_or_lt N n) as [Hn|Hn].
@@ -272,13 +272,13 @@ Section sequence.
   Proof.
     intro; induction  N as [| N HrecN].
     split with (Un 0); intros; rewrite (le_n_O_eq n H);
-      apply (Req_le (Un n) (Un n) (refl_equal (Un n))).
+      apply (Req_le (Un n) (Un n) (eq_refl (Un n))).
     elim HrecN; clear HrecN; intros; split with (Rmax (Un (S N)) x); intros;
       elim (Rmax_Rle (Un (S N)) x (Un n)); intros; clear H1;
         inversion H0.
     rewrite <- H1; rewrite <- H1 in H2;
       apply
-        (H2 (or_introl (Un n <= x) (Req_le (Un n) (Un n) (refl_equal (Un n))))).
+        (H2 (or_introl (Un n <= x) (Req_le (Un n) (Un n) (eq_refl (Un n))))).
     apply (H2 (or_intror (Un n <= Un (S N)) (H n H3))).
   Qed.
 
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 7c3b4699f..223649ef5 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -418,7 +418,7 @@ Proof.
   unfold D_x, no_cond in |- *.
   split.
   trivial.
-  apply (sym_not_eq (A:=R)); assumption.
+  apply (not_eq_sym (A:=R)); assumption.
   apply H5; assumption.
 Qed.
 
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v
index f1142d245..814e336c2 100644
--- a/theories/Reals/Rtopology.v
+++ b/theories/Reals/Rtopology.v
@@ -287,7 +287,7 @@ Proof.
   apply H5; split.
   unfold D_x, no_cond in |- *; split.
   trivial.
-  apply (sym_not_eq (A:=R)); apply H7.
+  apply (not_eq_sym (A:=R)); apply H7.
   unfold disc in H6; apply H6.
   intros; unfold continuity_pt in |- *; unfold continue_in in |- *;
     unfold limit1_in in |- *; unfold limit_in in |- *;
@@ -1581,7 +1581,7 @@ Proof.
   right; elim H1; intros; elim H2; intros; exists x; exists x0; intros.
   split;
     [ assumption
-      | split; [ assumption | apply (sym_not_eq (A:=R)); assumption ] ].
+      | split; [ assumption | apply (not_eq_sym (A:=R)); assumption ] ].
   left; exists x; split.
   assumption.
   intros; case (Req_dec x0 x); intro.
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
index 08fda178b..4a405660c 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -84,7 +84,7 @@ Proof.
   left; apply pow_lt; assumption.
   apply Rmult_le_reg_l with (INR (fact (S (S (2 * S n0 + 1))))).
   rewrite <- H3; apply lt_INR_0; apply neq_O_lt; red in |- *; intro;
-    assert (H5 := sym_eq H4); elim (fact_neq_0 _ H5).
+    assert (H5 := eq_sym H4); elim (fact_neq_0 _ H5).
   rewrite <- H3; rewrite (Rmult_comm (INR (fact (2 * S (S n0) + 1))));
     rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
   rewrite Rmult_1_r; rewrite H3; do 2 rewrite fact_simpl; do 2 rewrite mult_INR;
@@ -274,7 +274,7 @@ Proof.
   apply pow_le; assumption.
   apply Rmult_le_reg_l with (INR (fact (S (S (2 * S n1))))).
   rewrite <- H4; apply lt_INR_0; apply neq_O_lt; red in |- *; intro;
-    assert (H6 := sym_eq H5); elim (fact_neq_0 _ H6).
+    assert (H6 := eq_sym H5); elim (fact_neq_0 _ H6).
   rewrite <- H4; rewrite (Rmult_comm (INR (fact (2 * S (S n1)))));
     rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
   rewrite Rmult_1_r; rewrite H4; do 2 rewrite fact_simpl; do 2 rewrite mult_INR;
diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v
index 40989418c..90ba205f6 100644
--- a/theories/Reals/Rtrigo_calc.v
+++ b/theories/Reals/Rtrigo_calc.v
@@ -150,7 +150,7 @@ Proof.
         intro H2;
           [ assumption
             | absurd (0 = sqrt 2);
-              [ apply (sym_not_eq (A:=R)); apply sqrt2_neq_0 | assumption ] ] ].
+              [ apply (not_eq_sym (A:=R)); apply sqrt2_neq_0 | assumption ] ] ].
 Qed.
 
 Lemma Rlt_sqrt3_0 : 0 < sqrt 3.
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v
index c64931353..9b6edab68 100644
--- a/theories/Reals/Rtrigo_def.v
+++ b/theories/Reals/Rtrigo_def.v
@@ -130,17 +130,17 @@ Proof.
   intro; cut (0 <= up (/ eps))%Z.
   intro; assert (H2 := IZN _ H1); elim H2; intros; exists (max x 1).
   split.
-  cut (0 < IZR (Z_of_nat x)).
-  intro; rewrite INR_IZR_INZ; apply Rle_lt_trans with (/ IZR (Z_of_nat x)).
-  apply Rmult_le_reg_l with (IZR (Z_of_nat x)).
+  cut (0 < IZR (Z.of_nat x)).
+  intro; rewrite INR_IZR_INZ; apply Rle_lt_trans with (/ IZR (Z.of_nat x)).
+  apply Rmult_le_reg_l with (IZR (Z.of_nat x)).
   assumption.
   rewrite <- Rinv_r_sym;
     [ idtac | red in |- *; intro; rewrite H5 in H4; elim (Rlt_irrefl _ H4) ].
-  apply Rmult_le_reg_l with (IZR (Z_of_nat (max x 1))).
-  apply Rlt_le_trans with (IZR (Z_of_nat x)).
+  apply Rmult_le_reg_l with (IZR (Z.of_nat (max x 1))).
+  apply Rlt_le_trans with (IZR (Z.of_nat x)).
   assumption.
   repeat rewrite <- INR_IZR_INZ; apply le_INR; apply le_max_l.
-  rewrite Rmult_1_r; rewrite (Rmult_comm (IZR (Z_of_nat (max x 1))));
+  rewrite Rmult_1_r; rewrite (Rmult_comm (IZR (Z.of_nat (max x 1))));
     rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
   rewrite Rmult_1_r; repeat rewrite <- INR_IZR_INZ; apply le_INR;
     apply le_max_l.
diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v
index b77201411..04deb0904 100644
--- a/theories/Reals/Rtrigo_fun.v
+++ b/theories/Reals/Rtrigo_fun.v
@@ -39,7 +39,7 @@ Proof.
               in H4; rewrite (let (H1, H2) := Rmult_ne (/ INR (S n)) in H1) in H4;
                 rewrite (Rmult_comm (/ INR (S n))) in H4;
                   rewrite (Rmult_assoc eps (/ INR (S n)) (INR (S n))) in H4;
-                    rewrite (Rinv_l (INR (S n)) (not_O_INR (S n) (sym_not_equal (O_S n)))) in H4;
+                    rewrite (Rinv_l (INR (S n)) (not_O_INR (S n) (not_eq_sym (O_S n)))) in H4;
                       rewrite (let (H1, H2) := Rmult_ne eps in H1) in H4;
                         assumption.
   apply Rlt_minus; unfold Rgt in a; rewrite <- Rinv_1;
@@ -72,10 +72,10 @@ Proof.
               in H6; rewrite (let (H1, H2) := Rmult_ne (/ INR (S n)) in H1) in H6;
                 rewrite (Rmult_comm (/ INR (S n))) in H6;
                   rewrite (Rmult_assoc eps (/ INR (S n)) (INR (S n))) in H6;
-                    rewrite (Rinv_l (INR (S n)) (not_O_INR (S n) (sym_not_equal (O_S n)))) in H6;
+                    rewrite (Rinv_l (INR (S n)) (not_O_INR (S n) (not_eq_sym (O_S n)))) in H6;
                       rewrite (let (H1, H2) := Rmult_ne eps in H1) in H6;
                         assumption.
-  cut (IZR (up (/ eps - 1)) = IZR (Z_of_nat x));
+  cut (IZR (up (/ eps - 1)) = IZR (Z.of_nat x));
     [ intro | rewrite H1; trivial ].
   elim (archimed (/ eps - 1)); intros; clear H6; unfold Rgt in H5;
     rewrite H4 in H5; rewrite INR_IZR_INZ; assumption.
@@ -89,11 +89,11 @@ Proof.
     generalize (Rmult_lt_compat_l (/ eps) eps 1 (Rinv_0_lt_compat eps H) H0);
       rewrite
         (Rinv_l eps
-          (sym_not_eq (Rlt_dichotomy_converse 0 eps (or_introl (0 > eps) H))))
+          (not_eq_sym (Rlt_dichotomy_converse 0 eps (or_introl (0 > eps) H))))
         ; rewrite (let (H1, H2) := Rmult_ne (/ eps) in H1);
           intro; fold (/ eps - 1 > 0) in |- *; apply Rgt_minus;
             unfold Rgt in |- *; assumption.
-  right; rewrite H0; rewrite Rinv_1; apply sym_eq; apply Rminus_diag_eq; auto.
+  right; rewrite H0; rewrite Rinv_1; symmetry; apply Rminus_diag_eq; auto.
   elim (archimed (/ eps - 1)); intros; clear H1; unfold Rgt in H0; apply Rlt_le;
     assumption.
 Qed.
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index e5befbcf4..0a05e6df4 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -214,7 +214,7 @@ Proof.
   split.
   unfold D_x, no_cond in |- *; split.
   trivial.
-  apply (sym_not_eq (A:=R)); apply H6.
+  apply (not_eq_sym (A:=R)); apply H6.
   unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r; apply H7.
   unfold Boule in |- *; unfold Rminus in |- *; rewrite Ropp_0;
     rewrite Rplus_0_r; rewrite Rabs_R0; apply (cond_pos r).
@@ -298,7 +298,7 @@ Proof.
   split.
   unfold D_x, no_cond in |- *; split.
   trivial.
-  apply (sym_not_eq (A:=R)); unfold Rdiv in |- *; apply prod_neq_R0.
+  apply (not_eq_sym (A:=R)); unfold Rdiv in |- *; apply prod_neq_R0.
   apply H7.
   apply Rinv_neq_0_compat; discrR.
   apply Rlt_trans with (del_c / 2).
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 75c57401b..7b6eadc2f 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -1131,7 +1131,7 @@ Proof.
     rewrite Rinv_mult_distr.
   apply Rmult_le_compat_l.
   left; apply Rinv_0_lt_compat; apply lt_INR_0; apply neq_O_lt; red in |- *;
-    intro; assert (H10 := sym_eq H9); elim (fact_neq_0 _ H10).
+    intro; assert (H10 := eq_sym H9); elim (fact_neq_0 _ H10).
   left; apply Rinv_lt_contravar.
   apply Rmult_lt_0_compat; apply lt_INR_0; apply lt_O_Sn.
   apply lt_INR; apply lt_n_S.
@@ -1156,7 +1156,7 @@ Proof.
   replace (Rabs x ^ 1) with (Rabs x); [ idtac | simpl in |- *; ring ].
   replace (M_nat + n + 1)%nat with (S (M_nat + n)).
   apply Rmult_le_reg_l with (INR (fact (S (M_nat + n)))).
-  apply lt_INR_0; apply neq_O_lt; red in |- *; intro; assert (H9 := sym_eq H8);
+  apply lt_INR_0; apply neq_O_lt; red; intro; assert (H9 := eq_sym H8);
     elim (fact_neq_0 _ H9).
   rewrite (Rmult_comm (Rabs x)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym.
   rewrite Rmult_1_l.
@@ -1173,7 +1173,7 @@ Proof.
   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;
-    assert (H8 := sym_eq H7); elim (fact_neq_0 _ H8).
+    assert (H8 := eq_sym H7); elim (fact_neq_0 _ H8).
   clear Un Vn; apply INR_le; simpl in |- *.
   induction  M_nat as [| M_nat HrecM_nat].
   assert (H6 := archimed (Rabs x)); fold M in H6; elim H6; intros.
@@ -1192,7 +1192,7 @@ Proof.
   unfold Rdiv in |- *; rewrite Rabs_mult; rewrite (Rabs_right (/ INR (fact n))).
   rewrite RPow_abs; right; reflexivity.
   apply Rle_ge; left; apply Rinv_0_lt_compat; apply lt_INR_0; apply neq_O_lt;
-    red in |- *; intro; assert (H4 := sym_eq H3); elim (fact_neq_0 _ H4).
+    red; intro; assert (H4 := eq_sym H3); elim (fact_neq_0 _ H4).
   apply Rle_ge; unfold Rdiv in |- *; apply Rmult_le_pos.
   case (Req_dec x 0); intro.
   rewrite H3; rewrite Rabs_R0.
@@ -1201,6 +1201,6 @@ Proof.
       | simpl in |- *; rewrite Rmult_0_l; right; reflexivity ].
   left; apply pow_lt; apply Rabs_pos_lt; assumption.
   left; apply Rinv_0_lt_compat; apply lt_INR_0; apply neq_O_lt; red in |- *;
-    intro; assert (H4 := sym_eq H3); elim (fact_neq_0 _ H4).
+    intro; assert (H4 := eq_sym H3); elim (fact_neq_0 _ H4).
   apply H1; assumption.
 Qed.
diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v
index d00ed1786..4e704a274 100644
--- a/theories/Reals/Sqrt_reg.v
+++ b/theories/Reals/Sqrt_reg.v
@@ -250,7 +250,7 @@ Proof.
   unfold D_x, no_cond in |- *.
   split.
   trivial.
-  apply (sym_not_eq (A:=R)); exact H8.
+  apply (not_eq_sym (A:=R)); exact H8.
   unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r;
     apply Rlt_le_trans with alpha1.
   exact H9.