diff --git a/algebra/CGroups.v b/algebra/CGroups.v
index 5f7ab952..e44798da 100644
--- a/algebra/CGroups.v
+++ b/algebra/CGroups.v
@@ -337,7 +337,7 @@ Qed.
 End Assoc_properties.
 
 #[global]
-Hint Resolve assoc_2 minus_plus zero_minus cg_cancel_mixed plus_resp_eq:
+Hint Resolve assoc_2 Nat.add_sub zero_minus cg_cancel_mixed plus_resp_eq:
   algebra.
 
 
diff --git a/algebra/CPoly_Degree.v b/algebra/CPoly_Degree.v
index 17224f15..c8febc62 100644
--- a/algebra/CPoly_Degree.v
+++ b/algebra/CPoly_Degree.v
@@ -636,7 +636,7 @@ Proof.
     lia. lia. lia.
     apply H4; auto.
  intro. induction  k as [| k Hreck]; intros.
- apply H4. rewrite <- minus_n_O in H5; auto.
+ apply H4. rewrite Nat.sub_0_r in H5; auto.
   elim (le_lt_eq_dec (N - k) i); try intro y. auto. rewrite y in Hreck.
    apply mult_cancel_lft with (nth_coeff m p). auto. astepr ([0]:F).
    apply eq_transitive_unfolded with
diff --git a/fta/KeyLemma.v b/fta/KeyLemma.v
index 6d35d2d3..2b4bde0e 100644
--- a/fta/KeyLemma.v
+++ b/fta/KeyLemma.v
@@ -321,7 +321,7 @@ Proof.
  elim (le_gt_dec i j).
   auto.
  intro y.
- elim (le_not_gt _ _ H y).
+ elim (proj1 (Nat.le_ngt _ _) H y).
 Qed.
 
 Lemma chfun_2 : forall k j a i, j < i -> a = chfun k a j i.
@@ -330,7 +330,7 @@ Proof.
  unfold chfun in |- *.
  elim (le_gt_dec i j).
   intro y.
-  elim (le_not_gt _ _ y H).
+  elim (proj1 (Nat.le_ngt _ _) y H).
  auto.
 Qed.
 
diff --git a/ftc/FunctSeries.v b/ftc/FunctSeries.v
index 85c5396a..fb8a4205 100644
--- a/ftc/FunctSeries.v
+++ b/ftc/FunctSeries.v
@@ -740,7 +740,7 @@ Proof.
    exists N.
    exists 0.
    intro.
-   rewrite Nat.add_comm; rewrite Minus.minus_plus.
+   rewrite Nat.add_sub.
    algebra.
   Contin.
  intros x H0 n; induction  n as [| n Hrecn].
diff --git a/ftc/Partitions.v b/ftc/Partitions.v
index b3a4b235..de9f5b7d 100644
--- a/ftc/Partitions.v
+++ b/ftc/Partitions.v
@@ -705,9 +705,9 @@ Proof.
   exists (fun i : nat => i * k); repeat split.
     symmetry  in |- *; assumption.
    intros.
-   apply mult_lt_compat_r.
-    assumption.
+   apply Nat.mul_lt_mono_pos_r.
    apply Nat.neq_0_lt_0; auto.
+   assumption.
   intros.
   cut (i * k <= m).
    intro.
diff --git a/ftc/RefSepRef.v b/ftc/RefSepRef.v
index 323886e9..6f81fa25 100644
--- a/ftc/RefSepRef.v
+++ b/ftc/RefSepRef.v
@@ -399,8 +399,8 @@ Proof.
  elim (le_lt_dec n i); elim (le_lt_dec j 0); intros; simpl in |- *.
     elim (Nat.lt_irrefl 0); apply Nat.lt_le_trans with j; try apply Nat.le_lt_trans with i; auto with arith.
    elim (le_lt_dec n j); intro; simpl in |- *.
-    apply plus_lt_compat_l.
-    apply plus_lt_reg_l with n.
+    apply Nat.add_lt_mono_l.
+    apply Nat.add_lt_mono_l with n.
     repeat (rewrite Nat.add_comm; rewrite Nat.sub_add); auto.
    lia; auto; apply Nat.lt_trans with j; auto.
   elim (Nat.lt_irrefl 0); apply Nat.lt_trans with i; auto; apply Nat.lt_le_trans with j; auto.
@@ -479,7 +479,7 @@ Proof.
   intros.
   simpl in b0; rewrite <- b0; auto.
  elim (le_lt_eq_dec _ _ H); intro.
-  cut (pred i < pred n); [ intro | apply lt_pred; rewrite Nat.lt_succ_pred with 0 i; auto ].
+  cut (pred i < pred n); [ intro | apply Nat.lt_succ_lt_pred; rewrite Nat.lt_succ_pred with 0 i; auto ].
   cut (RSR_auxP i <= pred (m + n)).
    intro; exists H1.
    elim le_lt_eq_dec; intro; simpl in |- *.
@@ -590,8 +590,8 @@ Proof.
  elim (le_lt_dec m i); elim (le_lt_dec j 0); intros; simpl in |- *.
     elim (Nat.lt_irrefl 0); apply Nat.le_lt_trans with i; try apply Nat.lt_le_trans with j; auto with arith.
    elim (le_lt_dec m j); intro; simpl in |- *.
-    apply plus_lt_compat_l.
-    apply plus_lt_reg_l with m.
+    apply Nat.add_lt_mono_l.
+    apply Nat.add_lt_mono_l with m.
     repeat (rewrite Nat.add_comm; rewrite Nat.sub_add); auto.
    lia; auto; apply Nat.lt_trans with j; auto.
   elim (Nat.lt_irrefl 0); apply Nat.lt_trans with i; auto; apply Nat.lt_le_trans with j; auto.
@@ -702,9 +702,9 @@ Proof.
   elim (le_lt_dec j 0); intro; simpl in |- *.
    apply Nat.le_0_l.
   elim (le_lt_dec m j); intro; simpl in |- *.
-   rewrite not_le_minus_0.
+    rewrite (proj2 (Nat.sub_0_le j m)).
     rewrite <- plus_n_O; auto with arith.
-   apply Nat.lt_nge; auto.
+    assumption.
   apply plus_pred_pred_plus.
   elim (ProjT2 (RSR_h_g' _ (lt_pred' _ _ b1 b2))); intros.
   assumption.
diff --git a/ftc/RefSeparating.v b/ftc/RefSeparating.v
index f682dbfa..d1210a6a 100644
--- a/ftc/RefSeparating.v
+++ b/ftc/RefSeparating.v
@@ -291,7 +291,7 @@ Proof.
    apply less_wdl with (P (pred j) Hi'[-]P _ a0); intros.
     2: apply cg_minus_wd; apply prf1; auto.
    apply H0.
-   apply lt_pred_n_n.
+   apply Nat.lt_pred_l. apply Nat.neq_0_lt_0.
    apply Nat.le_lt_trans with (sep__part_h i).
     apply Nat.le_0_l.
    apply Partition_Points_mon with (P := P) (Hi := a0) (Hj := Hj).
diff --git a/liouville/nat_Q_lists.v b/liouville/nat_Q_lists.v
index 9cf171da..9aef5eae 100644
--- a/liouville/nat_Q_lists.v
+++ b/liouville/nat_Q_lists.v
@@ -180,14 +180,14 @@ Proof.
   rewrite H0.
   simpl.
   rewrite <- (Nat.add_0_r (Z.abs_nat a)) at 1.
-  apply plus_le_compat_l.
+  apply Nat.add_le_mono_l.
   apply Nat.le_0_l.
  simpl.
  destruct (ZL4 p).
  rewrite H0.
  simpl.
  rewrite <- (Nat.add_0_r (Z.abs_nat a)) at 1.
- apply plus_le_compat_l.
+ apply Nat.add_le_mono_l.
  apply Nat.le_0_l.
 Qed.
 
diff --git a/logic/CLogic.v b/logic/CLogic.v
index 9aaa23fd..4bd6922e 100644
--- a/logic/CLogic.v
+++ b/logic/CLogic.v
@@ -751,7 +751,7 @@ Lemma lt_5 : forall i n : nat, i < n -> pred i < n.
 Proof.
  intros; apply Nat.le_lt_trans with (pred n).
   apply Nat.pred_le_mono; auto with arith.
- apply lt_pred_n_n; apply Nat.le_lt_trans with i; auto with arith.
+ apply Nat.lt_pred_l; apply Nat.neq_0_lt_0. apply Nat.le_lt_trans with i; auto with arith.
 Qed.
 
 Lemma lt_8 : forall m n : nat, m < pred n -> m < n.
@@ -762,7 +762,7 @@ Qed.
 Lemma pred_lt : forall m n : nat, m < pred n -> S m < n.
 Proof.
  intros; apply Nat.le_lt_trans with (pred n); auto with arith.
- apply lt_pred_n_n; apply Nat.le_lt_trans with m.
+ apply Nat.lt_pred_l; apply Nat.neq_0_lt_0. apply Nat.le_lt_trans with m.
   auto with arith.
  apply Nat.lt_le_trans with (pred n); auto with arith.
 Qed.
diff --git a/model/Zmod/ZBasics.v b/model/Zmod/ZBasics.v
index 966c43b2..399c93d2 100644
--- a/model/Zmod/ZBasics.v
+++ b/model/Zmod/ZBasics.v
@@ -98,7 +98,7 @@ Lemma minus_n_minus_n_k : forall k n : nat, k <= n -> k = n - (n - k).
 Proof.
  intros k n Hle.
  induction  k as [| k Hreck].
-  rewrite <- minus_n_O.
+  rewrite Nat.sub_0_r.
   symmetry in |- *.
   apply Nat.sub_diag.
  set (K := k) in |- * at 2.
diff --git a/model/structures/Npossec.v b/model/structures/Npossec.v
index 3a25d649..15a6e179 100644
--- a/model/structures/Npossec.v
+++ b/model/structures/Npossec.v
@@ -87,15 +87,7 @@ Proof.
   cut ((x*S y0+x) > 0).
    unfold gt in |- *.
    intuition.
-  apply gt_trans with (x*S y0).
-   apply gt_le_trans with (x*S y0+0).
-    apply plus_gt_compat_l.
-    lia.
-   lia.
-  unfold gt in |- *.
-  apply Nat.neq_0_lt_0.
-  cut ((x*S y0) <> 0).
-   auto.
-  apply Hrecy0.
- auto.
+  apply Nat.lt_trans with (x*S y0).
+   apply Nat.lt_le_trans with (x*S y0+0).
+    lia. lia. lia. lia.
 Qed.
diff --git a/reals/Series.v b/reals/Series.v
index eaa7817c..60791287 100644
--- a/reals/Series.v
+++ b/reals/Series.v
@@ -804,7 +804,7 @@ Proof.
     (seq_part_sum x M[-]seq_part_sum x (S (Nat.max N M + k) - k))).
   apply AbsSmall_plus.
    apply HM.
-   apply (fun p n m : nat => plus_le_reg_l n m p) with k.
+   apply (fun p n m : nat => Nat.add_le_mono_l n m p) with k.
    rewrite (Nat.add_comm k (m- k)).
    rewrite Nat.sub_add.
     apply Nat.le_trans with (Nat.max N M + k); auto with arith.
@@ -812,7 +812,7 @@ Proof.
    apply Nat.le_trans with (S (Nat.max N M + k)); auto with arith.
   apply AbsSmall_minus.
   apply HM.
-  apply (fun p n m : nat => plus_le_reg_l n m p) with k.
+  apply (fun p n m : nat => Nat.add_le_mono_l n m p) with k.
   rewrite (Nat.add_comm k (S (Nat.max N M + k) - k)).
   rewrite Nat.sub_add.
    apply Nat.le_trans with (Nat.max N M + k); auto.
@@ -874,7 +874,7 @@ Proof.
   exists N.
   exists 0.
   intro.
-  rewrite Nat.add_comm; rewrite Minus.minus_plus.
+  rewrite Nat.add_sub.
   algebra.
  simple induction n.
   intro.
diff --git a/reals/fast/MultivariatePolynomials.v b/reals/fast/MultivariatePolynomials.v
index 221e201a..8ae34d24 100644
--- a/reals/fast/MultivariatePolynomials.v
+++ b/reals/fast/MultivariatePolynomials.v
@@ -306,8 +306,9 @@ Proof.
       rewrite <- (MVP_mult_apply Q_as_CRing).
       apply: MVP_apply_wd; try reflexivity.
       replace (proj1 (Nat.lt_succ_r n1 m) (Nat.lt_le_trans n1 (S n1) (S m) (Nat.lt_succ_diag_r n1) l))
-        with (Le.le_S_n n1 m l) by apply le_irrelevent.
-      apply c_mult_apply.
+        with (proj2 (Nat.succ_le_mono n1 m) l) by apply le_irrelevent.
+      replace (le_S_n n1 m l) with (proj2 (Nat.succ_le_mono n1 m) l) by apply le_irrelevent.
+      apply c_mult_apply. 
      apply MVP_BernsteinNonNeg; auto.
     eapply Qle_trans;[|apply Qmax_ub_r].
     set (R:=Vector.t_rec (MultivariatePolynomial Q_as_CRing n)
@@ -434,7 +435,8 @@ Proof.
      rewrite <- (MVP_mult_apply Q_as_CRing).
      apply: MVP_apply_wd; try reflexivity.
      replace (proj1 (Nat.lt_succ_r n1 m) (Nat.lt_le_trans n1 (S n1) (S m) (Nat.lt_succ_diag_r n1) l))
-       with (Le.le_S_n n1 m l) by apply le_irrelevent.
+       with (proj2 (Nat.succ_le_mono n1 m) l) by apply le_irrelevent.
+     replace (le_S_n n1 m l) with (proj2 (Nat.succ_le_mono n1 m) l) by apply le_irrelevent.
      apply c_mult_apply.
     apply MVP_BernsteinNonNeg; auto.
    eapply Qle_trans;[apply Qmin_lb_r|].
diff --git a/reals/stdlib/CMTFullSets.v b/reals/stdlib/CMTFullSets.v
index 8603622a..46c71c4b 100644
--- a/reals/stdlib/CMTFullSets.v
+++ b/reals/stdlib/CMTFullSets.v
@@ -1295,7 +1295,7 @@ Proof.
       unfold lt in l. simpl in xnlim.
       pose proof (xnlim (j - S i)%nat) as H0.
       replace (S (i + (j - S i)))%nat with j in H0. exact H0.
-      symmetry. exact (le_plus_minus_r (S i) j l). }
+      symmetry. rewrite Nat.add_comm. rewrite <- Nat.add_succ_r. exact (Nat.sub_add (S i) j l). }
     destruct (series_cv_abs
                 (fun n0 : nat => CRabs _ (partialApply (IntFn intRepres (S (i + n0))) x (xnlim n0)))
                 cau) as [x0 s].
diff --git a/stdlib_omissions/Z.v b/stdlib_omissions/Z.v
index e2c7f6e3..d5ee48ce 100644
--- a/stdlib_omissions/Z.v
+++ b/stdlib_omissions/Z.v
@@ -99,7 +99,7 @@ Qed.
 Lemma lt_Zlt_to_nat (n : nat) (z : Z) : Z.of_nat n < z <-> (n < Z.to_nat z)%nat.
 Proof.
 assert (A : forall (m n : nat), not (m <= n)%nat <-> (n < m)%nat).
-+ intros; split; [apply not_le | apply gt_not_le].
++ intros; split; [apply not_le | apply Nat.lt_nge].
 + assert (A1 := le_Zle_to_nat n z). apply iff_not in A1.
   now rewrite A, Z.nle_gt in A1.
 Qed.
diff --git a/util/Extract.v b/util/Extract.v
index cc5ed696..997f05b5 100644
--- a/util/Extract.v
+++ b/util/Extract.v
@@ -43,7 +43,7 @@ Extract Inlined Constant minus => "fun n m -> max 0 (n - m)".
 Extract Inlined Constant mult => "(*)".
 Extract Inlined Constant max => max.
 Extract Inlined Constant min => min.
-Extract Inlined Constant EqNat.beq_nat => "(==)".
+Extract Inlined Constant Nat.eqb => "(==)".
 Extract Inlined Constant EqNat.eq_nat_decide => "(==)".
 Extract Inlined Constant Peano_dec.eq_nat_dec => "(==)".