Remove deprecated Phase 2

NAux.v

@@ -104,7 +104,7 @@ Qed.
 Theorem Nmult_le_compat_l n m p : n <= m -> p * n <= p * m.
 Proof.
 intros H1; apply Nle_le; repeat rewrite N2Nat.inj_mul.
-apply mult_le_compat_l; apply le_Nle; repeat rewrite N2Nat.id; auto.
+apply Nat.mul_le_mono_l; apply le_Nle; repeat rewrite N2Nat.id; auto.
 Qed.
 
 Theorem Nmult_ge_compat_l n m p : n >= m -> p * n >= p * m.
@@ -240,10 +240,10 @@ Ltac set_to_nat :=
 Ltac to_nat := repeat to_nat_op; repeat set_to_nat.
 
 Theorem Nle_gt_trans n m p : m <= n -> m > p -> n > p.
-Proof. intros; to_nat; apply le_gt_trans with nn1; auto. Qed.
+Proof. intros; to_nat; apply Nat.lt_le_trans with nn1; auto. Qed.
 
 Theorem Ngt_le_trans n m p : n > m -> p <= m -> n > p.
-Proof. intros; to_nat; apply gt_le_trans with nn1; auto. Qed.
+Proof. intros; to_nat; apply Nat.le_lt_trans with nn1; auto. Qed.
 
 Theorem Nle_add_l x y : x <= y + x.
 Proof. intros; to_nat; auto with arith. Qed.

NatAux.v

@@ -73,14 +73,3 @@ Qed.
 
 Theorem le_0_eq_0 n : n <= 0 -> n = 0.
 Proof. case n; auto with arith. Qed.
-
-Definition le_gt_trans := Nat.lt_le_trans.
-Definition gt_le_trans := Nat.le_lt_trans.
-Definition mult_le_compat_l := Nat.mul_le_mono_l.
-Definition plus_le_compat_l := Nat.add_le_mono_l.
-Definition plus_le_reg_l := Nat.add_le_mono_l.
-Definition le_trans := Nat.le_trans.
-Definition plus_lt_reg_l := Nat.add_lt_mono_l.
-Definition plus_gt_reg_l := Nat.add_lt_mono_l.
-Definition plus_lt_compat_l := Nat.add_lt_mono_l.
-Definition plus_gt_compat_l :=  Nat.add_lt_mono_l.

PolAux.v

@@ -2,7 +2,6 @@ Require Import Qcanon.
 Require Export Replace2.
 Require Import NAux ZAux RAux.
 Require P.
-Require Import NatAux.
 
 (* Definition of the opposite for nat *)
 Definition Natopp := (fun x:nat => 0%nat).
@@ -211,13 +210,13 @@ Theorem plus_neg_compat_l a b c : b <> c -> a + b <> a + c.
 Proof. intros H H1; case H; apply Nat.add_cancel_l with a; auto. Qed.
 
 Theorem plus_ge_compat_l n m p : n >= m -> p + n >= p + m.
-Proof. intros H; unfold ge; apply plus_le_compat_l; auto. Qed.
+Proof. intros H; unfold ge; apply Nat.add_le_mono_l; auto. Qed.
 
 Theorem plus_neg_reg_l a b c : a + b <> a + c -> b <> c.
 Proof. intros H H1; case H; subst; auto. Qed.
 
 Theorem plus_ge_reg_l n m p : p + n >= p + m -> n >= m.
-Proof. intros H; unfold ge; apply plus_le_reg_l with p; auto. Qed.
+Proof. intros H; unfold ge; apply Nat.add_le_mono_l with p; auto. Qed.
 
 (* For replace *)
 
@@ -246,7 +245,7 @@ Theorem eq_ge_trans_r x y z : y = z -> x >= y -> x >= z.
 Proof. intros H; rewrite H; auto. Qed.
 
 Theorem ge_trans x y z : x >= z -> z >= y -> x >= y.
-Proof. intros H1 H2; red; apply le_trans with z; auto. Qed.
+Proof. intros H1 H2; red; apply Nat.le_trans with z; auto. Qed.
 
 Close Scope nat_scope.
 
@@ -276,13 +275,13 @@ Theorem Nplus_neg_reg_l a b c :  a + b <> a + c -> b <> c.
 Proof. intros H H1; case H; apply f_equal2 with (f:= Nplus); auto. Qed.
 
 Theorem Nplus_lt_reg_l n m p : p + n < p + m -> n < m.
-Proof. intros; to_nat; apply plus_lt_reg_l with nn1; auto with arith. Qed.
+Proof. intros; to_nat; apply Nat.add_lt_mono_l with nn1; auto with arith. Qed.
 
 Theorem Nplus_gt_reg_l: forall n m p, p + n > p + m -> n > m.
-Proof. intros; to_nat; apply plus_gt_reg_l with nn1; auto with arith. Qed.
+Proof. intros; to_nat; apply Nat.add_lt_mono_l with nn1; auto with arith. Qed.
 
 Theorem Nplus_le_reg_l n m p : p + n <= p + m -> n <= m.
-Proof. intros; to_nat; apply plus_le_reg_l with nn1; auto with arith. Qed.
+Proof. intros; to_nat; apply Nat.add_le_mono_l with nn1; auto with arith. Qed.
 
 Theorem Nplus_ge_reg_l n m p : p + n >= p + m -> n >= m.
 Proof. intros; to_nat; apply plus_ge_reg_l with nn1; auto with arith. Qed.
@@ -313,7 +312,7 @@ Theorem Neq_ge_trans_r x y z : y = z -> x >= y -> x >= z.
 Proof. intros H; rewrite H; auto. Qed.
 
 Theorem Nge_trans x y z : (x >= z) -> (z >= y) -> (x >= y).
-Proof. intros; to_nat; red; apply le_trans with nn1; auto with arith. Qed.
+Proof. intros; to_nat; red; apply Nat.le_trans with nn1; auto with arith. Qed.
 
 Close Scope N_scope.