diff --git a/algebra/Bernstein.v b/algebra/Bernstein.v
index 88f5c2ed..e1008971 100644
--- a/algebra/Bernstein.v
+++ b/algebra/Bernstein.v
@@ -59,12 +59,12 @@ end.
 
 (** These lemmas provide an induction principle for polynomials using the Bernstien basis *)
 Lemma Bernstein_inv1 : forall n i (H:i < n) (H0:S i <= S n),
- Bernstein H0[=]([1][-]_X_)[*](Bernstein (proj1 (Nat.lt_succ_r _ _) (lt_n_S _ _ H)))[+]_X_[*](Bernstein (le_S_n _ _ H0)).
+ Bernstein H0[=]([1][-]_X_)[*](Bernstein (proj1 (Nat.lt_succ_r _ _) (proj1 (Nat.succ_lt_mono _ _) H)))[+]_X_[*](Bernstein (le_S_n _ _ H0)).
 Proof.
  intros n i H H0.
  simpl (Bernstein H0).
  destruct (le_lt_eq_dec _ _ H0).
-  replace (proj1 (Nat.lt_succ_r (S i) n) l) with (proj1 (Nat.lt_succ_r _ _) (lt_n_S _ _ H)) by apply le_irrelevent.
+  replace (proj1 (Nat.lt_succ_r (S i) n) l) with (proj1 (Nat.lt_succ_r _ _) (proj1 (Nat.succ_lt_mono _ _) H)) by apply le_irrelevent.
   reflexivity.
  exfalso; lia.
 Qed.
@@ -176,7 +176,7 @@ Proof.
   rstepr (Bernstein (le_n_S 0 (S n) H)).
   set (le_n_S 0 n (Nat.le_0_l n)).
   rewrite (Bernstein_inv1 l).
-  rewrite (le_irrelevent _ _ (proj1 (Nat.lt_succ_r 1 (S n)) (lt_n_S 0 (S n) l)) l).
+  rewrite (le_irrelevent _ _ (proj1 (Nat.lt_succ_r 1 (S n)) (proj1 (Nat.succ_lt_mono 0 (S n)) l)) l).
   rewrite (le_irrelevent _ _ H (le_S_n 0 (S n) (le_n_S 0 (S n) H))).
   reflexivity.
  simpl (Bernstein H) at 1.
@@ -189,7 +189,7 @@ Proof.
   replace (le_n_S i n (le_S_n i n H)) with H by apply le_irrelevent.
   rstepl ((nring (S i)[+][1])[*](([1][-]_X_)[*]Bernstein l0[+]_X_[*]Bernstein H)).
   rewrite (Bernstein_inv1 l).
-  replace (proj1 (Nat.lt_succ_r (S (S i)) (S n)) (lt_n_S (S i) (S n) l)) with l0 by apply le_irrelevent.
+  replace (proj1 (Nat.lt_succ_r (S (S i)) (S n)) (proj1 (Nat.succ_lt_mono (S i) (S n)) l)) with l0 by apply le_irrelevent.
   replace (le_S_n (S i) (S n) (le_n_S (S i) (S n) H)) with H by apply le_irrelevent.
   reflexivity.
  rstepl (_X_[*](nring (S n)[*]_X_[*]Bernstein (proj1 (Nat.lt_succ_r _ _) H))[+] _X_[*]Bernstein H).
@@ -240,7 +240,7 @@ Proof.
   rstepl ((nring (n - i)[+][1])[*](X0[*]Bernstein H[+]_X_[*]Bernstein l0)).
   rewrite -> (Bernstein_inv1 H).
   fold X0.
-  replace (proj1 (Nat.lt_succ_r _ _) (lt_n_S _ _ H)) with H by apply le_irrelevent.
+  replace (proj1 (Nat.lt_succ_r _ _) (proj1 (Nat.succ_lt_mono _ _) H)) with H by apply le_irrelevent.
   replace (le_S_n _ _ (le_S (S i) (S n) H)) with l0 by apply le_irrelevent.
   reflexivity.
  revert H.
@@ -256,7 +256,7 @@ Proof.
  replace (S (S n) - S n) with 1 by auto with *.
  replace (le_S_n n (S n) (le_S (S n) (S n) H))
    with (le_S n n (proj1 (Nat.lt_succ_r n n) H)) by apply le_irrelevent.
- replace (proj1 (Nat.lt_succ_r (S n) (S n)) (lt_n_S n (S n) l)) with H by apply le_irrelevent.
+ replace (proj1 (Nat.lt_succ_r (S n) (S n)) (proj1 (Nat.succ_lt_mono n (S n)) l)) with H by apply le_irrelevent.
  ring.
 Qed.
 
diff --git a/algebra/COrdCauchy.v b/algebra/COrdCauchy.v
index 061c8713..0dd60198 100644
--- a/algebra/COrdCauchy.v
+++ b/algebra/COrdCauchy.v
@@ -266,9 +266,9 @@ Proof.
   apply less_leEq_trans with e; eauto with arith.
  unfold CS_seq_recip_seq in |- *.
  elim lt_le_dec; intro; simpl in |- *.
-  exfalso; apply le_not_lt with N n; eauto with arith.
+  exfalso; apply Nat.le_ngt with N n; eauto with arith.
  elim lt_le_dec; intro; simpl in |- *.
-  exfalso; apply le_not_lt with N (Nat.max K N); eauto with arith.
+  exfalso; apply Nat.le_ngt with N (Nat.max K N); eauto with arith.
  rstepr (f (Nat.max K N)[-]f n).
  apply AbsSmall_leEq_trans with (d[*]e[*]e).
   apply mult_resp_leEq_both.
diff --git a/algebra/COrdFields2.v b/algebra/COrdFields2.v
index 08ef265f..c10ec1ff 100644
--- a/algebra/COrdFields2.v
+++ b/algebra/COrdFields2.v
@@ -797,9 +797,9 @@ Proof.
   assumption.
  intros.
  elim (le_lt_dec m i); intro;
-   [ simpl in |- * | exfalso; apply (le_not_lt m i); auto with arith ].
+   [ simpl in |- * | exfalso; apply (Nat.le_ngt m i); auto with arith ].
  elim (le_lt_dec i n); intro;
-   [ simpl in |- * | exfalso; apply (le_not_lt i n); auto with arith ].
+   [ simpl in |- * | exfalso; apply (Nat.le_ngt i n); auto with arith ].
  apply H0.
 Qed.
 
diff --git a/algebra/CPoly_Degree.v b/algebra/CPoly_Degree.v
index 009ec397..17224f15 100644
--- a/algebra/CPoly_Degree.v
+++ b/algebra/CPoly_Degree.v
@@ -457,13 +457,13 @@ Proof.
    simpl in |- *. auto with arith.
   induction  p as [| s p Hrecp]; intros.
   simpl in H. elim (ap_irreflexive_unfolded _ _ H).
-  simpl in |- *. simpl in H. apply lt_n_S. auto.
+  simpl in |- *. simpl in H. apply -> Nat.succ_lt_mono. auto.
 Qed.
 
 Lemma poly_degree_lth : forall p : RX, degree_le (lth_of_poly p) p.
 Proof.
  unfold degree_le in |- *. intros. apply not_ap_imp_eq. intro.
- elim (lt_not_le _ _ H). apply Nat.lt_le_incl.
+ elim (proj1 (Nat.lt_nge _ _) H). apply Nat.lt_le_incl.
  apply lt_i_lth_of_poly. auto.
 Qed.
 
@@ -495,7 +495,7 @@ Proof.
   cut (i <> i0). intro.
   Step_final (nth_coeff i0 p[*][0]).
  intro; rewrite <- H2 in H1.
- apply (le_not_lt i n); auto.
+ apply (Nat.le_ngt i n); auto.
 Qed.
 
 Hint Resolve poly_as_sum'': algebra.
diff --git a/algebra/CSums.v b/algebra/CSums.v
index 84ee5ce7..d592ecfe 100644
--- a/algebra/CSums.v
+++ b/algebra/CSums.v
@@ -87,7 +87,7 @@ Proof.
  intros n f Hf i Hi.
  unfold part_tot_nat_fun in |- *.
  elim le_lt_dec; intro.
-  exfalso; apply (le_not_lt n i); auto.
+  exfalso; apply (Nat.le_ngt n i); auto.
  simpl in |- *; apply Hf; auto.
 Qed.
 
@@ -98,7 +98,7 @@ Proof.
  unfold part_tot_nat_fun in |- *.
  elim le_lt_dec; intro.
   simpl in |- *; algebra.
- exfalso; apply (le_not_lt n i); auto.
+ exfalso; apply (Nat.le_ngt n i); auto.
 Qed.
 
 (** [Sum0] defines the sum for [i=0..(n-1)] *)
@@ -365,8 +365,8 @@ Proof.
  apply Sum_wd'.
   assumption.
  intros i H1 H2.
- elim le_lt_dec; intro H3; [ simpl in |- * | exfalso; apply (le_not_lt i n); auto ].
- elim le_lt_dec; intro H4; [ simpl in |- * | exfalso; apply (le_not_lt m i); auto ].
+ elim le_lt_dec; intro H3; [ simpl in |- * | exfalso; apply (Nat.le_ngt i n); auto ].
+ elim le_lt_dec; intro H4; [ simpl in |- * | exfalso; apply (Nat.le_ngt m i); auto ].
  algebra.
 Qed.
 
diff --git a/algebra/Cauchy_COF.v b/algebra/Cauchy_COF.v
index 34dadd2e..c00698e3 100644
--- a/algebra/Cauchy_COF.v
+++ b/algebra/Cauchy_COF.v
@@ -592,7 +592,7 @@ Proof.
     eapply leEq_wdr.
      apply (HM (Nat.max K N)); auto with arith.
     unfold CS_seq_recip_seq in |- *; elim lt_le_dec; intro.
-     exfalso; apply le_not_lt with N (Nat.max K N); auto with arith.
+     exfalso; apply Nat.le_ngt with N (Nat.max K N); auto with arith.
     simpl in |- *; rational.
    apply (less_irreflexive_unfolded _ d).
    apply leEq_less_trans with ([0]:F); auto.
@@ -600,7 +600,7 @@ Proof.
    eapply leEq_wdr.
     apply (HM (Nat.max K N)); auto with arith.
    unfold CS_seq_recip_seq in |- *; elim lt_le_dec; intro.
-    exfalso; apply le_not_lt with N (Nat.max K N); auto with arith.
+    exfalso; apply Nat.le_ngt with N (Nat.max K N); auto with arith.
    simpl in |- *; rational.
   apply (less_irreflexive_unfolded _ d).
   apply leEq_less_trans with ([0]:F); auto.
@@ -608,7 +608,7 @@ Proof.
   eapply leEq_wdr.
    apply (HM (Nat.max K N)); auto with arith.
   unfold CS_seq_recip_seq in |- *; elim lt_le_dec; intro.
-   exfalso; apply le_not_lt with N (Nat.max K N); auto with arith.
+   exfalso; apply Nat.le_ngt with N (Nat.max K N); auto with arith.
   simpl in |- *; rational.
  apply (less_irreflexive_unfolded _ d).
  apply leEq_less_trans with ([0]:F); auto.
@@ -616,7 +616,7 @@ Proof.
  eapply leEq_wdr.
   apply (HM (Nat.max K N)); auto with arith.
  unfold CS_seq_recip_seq in |- *; elim lt_le_dec; intro.
-  exfalso; apply le_not_lt with N (Nat.max K N); auto with arith.
+  exfalso; apply Nat.le_ngt with N (Nat.max K N); auto with arith.
  simpl in |- *; rational.
 Qed.
 
diff --git a/ftc/COrdLemmas.v b/ftc/COrdLemmas.v
index de24b88f..9a4a3080 100644
--- a/ftc/COrdLemmas.v
+++ b/ftc/COrdLemmas.v
@@ -347,7 +347,7 @@ Proof.
       exfalso; lia.
      elim (le_lt_dec (f (S n)) i); intro; simpl in |- *.
       cut (f n < f (S n)); [ intro | apply f_mon; apply Nat.lt_succ_diag_r ].
-      exfalso; apply (le_not_lt (f n) i); auto.
+      exfalso; apply (Nat.le_ngt (f n) i); auto.
       apply Nat.le_trans with (f (S n)); auto with arith.
      intros; unfold part_tot_nat_fun in |- *;
        elim (le_lt_dec (f (S n)) i);elim (le_lt_dec (f n) i);simpl;intros; try reflexivity;try exfalso; try lia.
@@ -443,7 +443,7 @@ Proof.
        intro.
        rewrite <- H6.
        rewrite <- plus_n_Sm; auto with arith.
-      exfalso; apply (le_not_lt i m); auto with arith.
+      exfalso; apply (Nat.le_ngt i m); auto with arith.
      set (x := f m (le_n m)) in *; clearbody x; auto with arith.
     assumption.
    intros.
@@ -458,7 +458,7 @@ Proof.
  unfold f' in |- *.
  elim (le_lt_dec i m); intro; simpl in |- *.
   apply H0; auto.
- elim (le_not_lt i m); auto.
+ lia; auto.
 Qed.
 
 End More_Lemmas.
diff --git a/ftc/FunctSums.v b/ftc/FunctSums.v
index 49ccf850..6062fdf4 100644
--- a/ftc/FunctSums.v
+++ b/ftc/FunctSums.v
@@ -390,7 +390,7 @@ Proof.
  do 6 intro.
  unfold FSumx_to_FSum in |- *.
  elim (le_lt_dec n i); intro; simpl in |- *.
-  exfalso; apply (le_not_lt n i); auto.
+  exfalso; apply (Nat.le_ngt n i); auto.
  intros; apply H; auto.
  algebra.
 Qed.
@@ -402,7 +402,7 @@ Proof.
  unfold FSumx_to_FSum in |- *.
  elim (le_lt_dec n i); intro; simpl in |- *.
   intro; algebra.
- intros; exfalso; apply (le_not_lt n i); auto.
+ intros; exfalso; apply (Nat.le_ngt n i); auto.
 Qed.
 
 Lemma FSum_FSumx_to_FSum : forall n (f : forall i, i < S n -> PartIR),
diff --git a/ftc/Integral.v b/ftc/Integral.v
index 513e309a..eb127e45 100644
--- a/ftc/Integral.v
+++ b/ftc/Integral.v
@@ -750,7 +750,7 @@ Proof.
  intros; unfold partition_join_fun in |- *.
  elim le_lt_dec; intro; simpl in |- *.
   apply prf1; auto.
- exfalso; apply le_not_lt with i n; auto.
+ exfalso; apply Nat.le_ngt with i n; auto.
 Qed.
 
 Lemma pjf_2 : forall (i : nat) Hi, i = n -> partition_join_fun i Hi [=] c.
@@ -781,7 +781,7 @@ Proof.
  intros; unfold partition_join_fun in |- *.
  generalize Hj; rewrite H0; clear Hj; intros.
  elim le_lt_dec; intro; simpl in |- *.
-  exfalso; apply le_not_lt with i n; auto.
+  exfalso; apply Nat.le_ngt with i n; auto.
  apply prf1; auto.
 Qed.
 
@@ -792,10 +792,10 @@ Proof.
  unfold partition_join_fun in |- *.
  elim (le_lt_dec i n); elim (le_lt_dec j n); intros; simpl in |- *.
     apply prf1; auto.
-   exfalso; apply le_not_lt with i n.
+   exfalso; apply Nat.le_ngt with i n.
     assumption.
    rewrite H; assumption.
-  exfalso; apply le_not_lt with j n.
+  exfalso; apply Nat.le_ngt with j n.
    assumption.
   rewrite <- H; assumption.
  apply prf1; auto.
@@ -818,7 +818,7 @@ Proof.
    apply eq_transitive_unfolded with (Q 0 (Nat.le_0_l _)).
     apply eq_symmetric_unfolded; apply start.
    apply prf1; auto with arith.
-  exfalso; apply le_not_lt with n i; auto with arith.
+  exfalso; apply Nat.le_ngt with n i; auto with arith.
  cut (i - n = S (i - S n)); [ intro | lia ].
  cut (S (i - S n) <= m); [ intro | lia ].
  apply leEq_wdr with (Q _ H1).
@@ -896,7 +896,7 @@ Proof.
   elim le_lt_eq_dec; intro; simpl in |- *.
    algebra.
   exfalso; rewrite b0 in Hi'; apply (Nat.lt_irrefl _ Hi').
- exfalso; apply le_not_lt with i n; auto with arith.
+ exfalso; apply Nat.le_ngt with i n; auto with arith.
 Qed.
 
 Lemma pjp_2 : forall (i : nat) Hi, i = n -> partition_join_pts i Hi [=] c.
@@ -914,7 +914,7 @@ Lemma pjp_3 : forall (i : nat) Hi Hi',
 Proof.
  intros; unfold partition_join_pts in |- *.
  elim le_lt_dec; intro; simpl in |- *.
-  exfalso; apply le_not_lt with i n; auto.
+  exfalso; apply Nat.le_ngt with i n; auto.
  cut (fQ _ (partition_join_aux' _ _ _ b0 Hi) [=] fQ _ Hi').
   2: apply HfQ'; auto.
  algebra.
@@ -952,7 +952,7 @@ Proof.
    cut (forall H, Q (n - n) H [=] c); auto.
    cut (n - n = 0); [ intro | auto with arith ].
    rewrite H1; intros; apply start.
-  exfalso; apply le_not_lt with n i; auto with arith.
+  exfalso; apply Nat.le_ngt with n i; auto with arith.
  elim (HfQ _ (partition_join_aux' _ _ _ b1 H)); intros.
  apply compact_wd with (fQ _ (partition_join_aux' _ _ _ b1 H)).
   2: apply eq_symmetric_unfolded; apply pjp_3; assumption.
@@ -1011,9 +1011,9 @@ Proof.
     apply pfwdef; apply eq_symmetric_unfolded; apply pjp_1.
    apply cg_minus_wd; simpl in |- *.
     unfold partition_join_fun in |- *; elim le_lt_dec; simpl in |- *; intro; [ apply prf1; auto
-      | exfalso; apply le_not_lt with n i; auto with arith ].
+      | exfalso; apply Nat.le_ngt with n i; auto with arith ].
    unfold partition_join_fun in |- *; elim le_lt_dec; simpl in |- *; intro; [ apply prf1; auto
-     | exfalso; apply le_not_lt with i n; auto with arith ].
+     | exfalso; apply Nat.le_ngt with i n; auto with arith ].
   intros; apply mult_wd.
    apply pfwdef.
    cut (i = S (n + i) - S n); [ intro | lia ].
@@ -1071,7 +1071,7 @@ Proof.
    eapply leEq_transitive.
     apply Mesh_lemma.
    apply lft_leEq_Max.
-  exfalso; apply le_not_lt with i n; auto with arith.
+  exfalso; apply Nat.le_ngt with i n; auto with arith.
  elim le_lt_dec; intro; simpl in |- *.
   cut (i = n); [ intro | apply Nat.le_antisymm; auto with arith ].
   generalize a0 b0 Hi'; clear Hx Hi Hi' a0 b0.
@@ -1182,7 +1182,7 @@ Proof.
         elim le_lt_eq_dec; intro; simpl in |- *.
          apply Partition_imp_points_2; auto.
         exfalso; rewrite b0 in Hi; apply (Nat.lt_irrefl _ Hi).
-       exfalso; apply le_not_lt with i0 (S i); auto with arith.
+       exfalso; apply Nat.le_ngt with i0 (S i); auto with arith.
       apply cg_minus_wd; simpl in |- *.
        apply eq_symmetric_unfolded; apply pjf_1.
       apply eq_symmetric_unfolded; apply pjf_1.
diff --git a/ftc/Partitions.v b/ftc/Partitions.v
index 509f01c4..a9e7cce4 100644
--- a/ftc/Partitions.v
+++ b/ftc/Partitions.v
@@ -243,7 +243,7 @@ Proof.
    cut (f j < f n); [ intro | apply Nat.le_lt_trans with i; auto ].
    apply not_ge.
    intro; red in H1.
-   apply (le_not_lt (f j) (f n)); auto with arith.
+   apply (Nat.le_ngt (f j) (f n)); auto with arith.
    apply Hfmon.
    elim (le_lt_eq_dec _ _ H1); intro; auto.
    rewrite b0 in H0; elim (Nat.lt_irrefl (f j)); auto.
diff --git a/ftc/RefLemma.v b/ftc/RefLemma.v
index cb8e24ce..5915cdd6 100644
--- a/ftc/RefLemma.v
+++ b/ftc/RefLemma.v
@@ -264,23 +264,23 @@ Proof.
      elim (le_lt_dec (S j) m); intro; simpl in |- *.
       apply prf1; auto.
      cut (S j <= m); [ intro | apply H' with i; assumption ].
-     exfalso; apply (le_not_lt _ _ H2 b0).
+     exfalso; apply (proj1 (Nat.le_ngt _ _) H2 b0).
     elim (le_lt_dec j m); intro; simpl in |- *.
      apply prf1; auto.
     cut (j < m); [ intro | apply H with i; assumption ].
-    exfalso; apply le_not_lt with m j; auto with arith.
-   exfalso; apply le_not_lt with (sub i) j; auto with arith.
-  exfalso; apply (le_not_lt _ _ Hj' b0).
+    exfalso; apply Nat.le_ngt with m j; auto with arith.
+   exfalso; apply Nat.le_ngt with (sub i) j; auto with arith.
+  exfalso; apply (proj1 (Nat.le_ngt _ _) Hj' b0).
  unfold h in |- *.
  apply cg_minus_wd.
   elim (le_lt_dec (S (pred (sub (S i)))) m); intro; simpl in |- *.
    apply prf1; auto.
   exfalso.
-  apply (le_not_lt _ _ P1 b0).
+  apply (proj1 (Nat.le_ngt _ _) P1 b0).
  elim (le_lt_dec (sub i) m); intro; simpl in |- *.
   apply prf1; auto.
  exfalso.
- apply (le_not_lt _ _ P2 b0).
+ apply (proj1 (Nat.le_ngt _ _) P2 b0).
 Qed.
 
 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)).
@@ -329,21 +329,21 @@ Proof.
       exfalso.
       cut (0 < sub (S i)); [ intro | apply RL_sub_S ].
       cut (sub (S i) <= m); intros.
-       apply (le_not_lt _ _ H4); apply Nat.le_lt_trans with j; auto.
+       apply (proj1 (Nat.le_ngt _ _) H4); apply Nat.le_lt_trans with j; auto.
       rewrite <- RL_sub_n.
       apply RL_sub_mon'; apply Hi.
      apply mult_wd.
       apply pfwdef.
       apply HfQ'; auto.
      apply cg_minus_wd; apply prf1; auto.
-    exfalso; apply (le_not_lt _ _ b0).
+    exfalso; apply (proj1 (Nat.le_ngt _ _) b0).
     rewrite (Nat.lt_succ_pred _ _ (RL_sub_S i)); auto.
-   exfalso; apply (le_not_lt _ _ H1 b0).
+   exfalso; apply (proj1 (Nat.le_ngt _ _) H1 b0).
   symmetry  in |- *; apply RL_sub_n.
  apply Sumx_wd; intros.
  unfold part_tot_nat_fun in |- *.
  elim (le_lt_dec m i); intro; simpl in |- *.
-  exfalso; apply le_not_lt with m i; auto.
+  exfalso; apply Nat.le_ngt with m i; auto.
  apply mult_wd.
   apply pfwdef; apply HfQ'; auto.
  apply cg_minus_wd; apply prf1; auto.
diff --git a/ftc/RefSepRef.v b/ftc/RefSepRef.v
index d25b0979..82add500 100644
--- a/ftc/RefSepRef.v
+++ b/ftc/RefSepRef.v
@@ -352,7 +352,7 @@ Proof.
  intros.
  unfold RSR_auxP in |- *.
  elim (le_lt_dec n i); intro; simpl in |- *.
-  exfalso; apply le_not_lt with n i; auto.
+  exfalso; apply Nat.le_ngt with n i; auto.
  elim (le_lt_dec i 0); intro; simpl in |- *.
   exfalso; apply Nat.lt_irrefl with 0; apply Nat.lt_le_trans with i; auto.
  set (x := ProjT1 (RSR_h_f' _ (lt_pred' _ _ b1 b0))) in *.
@@ -402,11 +402,11 @@ Proof.
     apply plus_lt_compat_l.
     apply plus_lt_reg_l with n.
     repeat rewrite <- le_plus_minus; auto.
-   elim (le_not_lt n i); auto; apply Nat.lt_trans with j; 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.
  elim (le_lt_dec n j); intro; simpl in |- *.
   apply Nat.lt_le_trans with (S (pred m + pred n)).
-   apply lt_n_S.
+   apply -> Nat.succ_lt_mono.
    apply (ProjT1 (ProjT2 (RSR_h_f' (pred i) (lt_pred' _ _ b0 b2)))).
   rewrite plus_n_Sm.
   rewrite Nat.lt_succ_pred with 0 n.
@@ -421,7 +421,7 @@ Proof.
   apply Nat.lt_irrefl with 0.
   apply Nat.lt_trans with i; auto.
   rewrite RSR_mn0; auto.
- apply lt_n_S.
+ apply -> Nat.succ_lt_mono.
  cut (~ ~ ProjT1 (RSR_h_f' (pred i) (lt_pred' _ _ b0 b2)) <
    ProjT1 (RSR_h_f' (pred j) (lt_pred' _ _ b1 b3))); intro.
   apply not_not_lt; assumption.
@@ -543,7 +543,7 @@ Proof.
  intros.
  unfold RSR_auxR in |- *.
  elim (le_lt_dec m i); intro; simpl in |- *.
-  exfalso; apply le_not_lt with m i; auto.
+  exfalso; apply Nat.le_ngt with m i; auto.
  elim (le_lt_dec i 0); intro; simpl in |- *.
   exfalso; apply Nat.lt_irrefl with 0; apply Nat.lt_le_trans with i; auto.
  set (x := ProjT1 (RSR_h_g' _ (lt_pred' _ _ b1 b0))) in *.
@@ -593,11 +593,11 @@ Proof.
     apply plus_lt_compat_l.
     apply plus_lt_reg_l with m.
     repeat rewrite <- le_plus_minus; auto.
-   elim (le_not_lt m i); auto; apply Nat.lt_trans with j; 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.
  elim (le_lt_dec m j); intro; simpl in |- *.
   set (H0 := RSR_nm0) in *; set (H1 := RSR_mn0) in *; apply Nat.lt_le_trans with (S (pred m + pred n)).
-   apply lt_n_S.
+   apply -> Nat.succ_lt_mono.
    apply (ProjT1 (ProjT2 (RSR_h_g' (pred i) (lt_pred' _ _ b0 b2)))).
   rewrite <- plus_Sn_m.
   rewrite Nat.lt_succ_pred with 0 m.
@@ -615,7 +615,7 @@ Proof.
   apply Nat.lt_irrefl with 0.
   apply Nat.lt_trans with i; auto.
   rewrite RSR_nm0; auto.
- apply lt_n_S.
+ apply -> Nat.succ_lt_mono.
  cut (~ ~ ProjT1 (RSR_h_g' (pred i) (lt_pred' _ _ b0 b2)) <
    ProjT1 (RSR_h_g' (pred j) (lt_pred' _ _ b1 b3))); intro.
   apply not_not_lt; assumption.
@@ -704,7 +704,7 @@ Proof.
   elim (le_lt_dec m j); intro; simpl in |- *.
    rewrite not_le_minus_0.
     rewrite <- plus_n_O; auto with arith.
-   apply lt_not_le; auto.
+   apply Nat.lt_nge; auto.
   apply plus_pred_pred_plus.
   elim (ProjT2 (RSR_h_g' _ (lt_pred' _ _ b1 b2))); intros.
   assumption.
diff --git a/ftc/RefSeparated.v b/ftc/RefSeparated.v
index 907aff8a..99afd5a5 100644
--- a/ftc/RefSeparated.v
+++ b/ftc/RefSeparated.v
@@ -205,7 +205,7 @@ Proof.
      intros; apply HR.
     red in |- *; intros; apply prf1; auto.
    assumption.
-  exfalso; apply (le_not_lt j' m); auto.
+  exfalso; apply (Nat.le_ngt j' m); auto.
  elim (le_lt_dec j 0); intro.
   exfalso; apply Nat.nlt_0_r with j'; red in |- *; apply Nat.le_trans with j; auto.
  generalize Hj H H0; clear H0 H Hj.
@@ -289,7 +289,7 @@ Proof.
     apply b0.
    apply AbsIR_wd; apply cg_minus_wd; apply prf1; auto.
   left; intro.
-  exfalso; apply le_not_lt with i n; auto.
+  exfalso; apply Nat.le_ngt with i n; auto.
  intros.
  apply less_cotransitive_unfolded.
  rstepl ((delta [/]TwoNZ) [/]TwoNZ).
diff --git a/ftc/RefSeparating.v b/ftc/RefSeparating.v
index 69a02818..7027e482 100644
--- a/ftc/RefSeparating.v
+++ b/ftc/RefSeparating.v
@@ -274,7 +274,7 @@ Proof.
   apply local_mon'_imp_mon'2_le with (f := fun (i : nat) Hi => P i Hi).
    intros; apply prf2.
   assumption.
- exfalso; apply (le_not_lt _ _ Hi b0).
+ exfalso; lia.
 Qed.
 
 Lemma sep__part_h_lemma2 :
@@ -303,7 +303,7 @@ Proof.
   unfold cg_minus in |- *; apply plus_resp_leEq_both.
    apply Partition_mon; assumption.
   apply inv_resp_leEq; apply eq_imp_leEq; apply prf1; auto.
- exfalso; exact (le_not_lt _ _ (sep__part_h_bnd _) b0).
+ exfalso; lia.
 Qed.
 
 Lemma sep__part_h_lemma3 :
@@ -691,7 +691,7 @@ Proof.
      apply cg_minus_wd; apply prf1; auto.
     astepl ([0][+]delta [/]TwoNZ); apply plus_resp_leEq; apply Mesh_nonneg.
    exfalso.
-   exact (le_not_lt _ _ (sep__part_h_bnd _) b2).
+   lia.
   rstepl (Mesh P[+]delta).
   apply plus_resp_leEq_lft; apply RS'_delta_csi.
  elim (ProjT2 sep__part_app_n); fold RS'_m1 in |- *; intros.
@@ -815,26 +815,26 @@ Proof.
      unfold h in |- *.
      do 2 elim le_lt_dec; intros; simpl in |- *.
         apply cg_minus_wd; apply prf1; auto.
-       exfalso; apply le_not_lt with j n.
+       exfalso; apply Nat.le_ngt with j n.
         apply Nat.le_trans with (S j); auto with arith.
        assumption.
-      exfalso; apply le_not_lt with (S j) n.
+      exfalso; apply Nat.le_ngt with (S j) n.
        exact (RS'_Hsep_S _ _ Hi a1).
       assumption.
-     exfalso; apply le_not_lt with (S j) n.
+     exfalso; apply Nat.le_ngt with (S j) n.
       exact (RS'_Hsep_S _ _ Hi a1).
      assumption.
-    exfalso; exact (le_not_lt _ _ H1 b0).
-   exfalso; exact (le_not_lt _ _ H2 b0).
-  exfalso; exact (le_not_lt _ _ H1 b0).
+    exfalso; lia.
+   exfalso; lia.
+  exfalso; lia.
  unfold h in |- *.
  apply cg_minus_wd.
   elim le_lt_dec; simpl in |- *; intros.
    apply prf1; auto.
-  exfalso; exact (le_not_lt _ _ H0 b0).
+  exfalso; lia.
  elim le_lt_dec; intro; simpl in |- *.
   apply prf1; auto.
- exfalso; rewrite <- H in H0; apply le_not_lt with (sep__part_fun i (Nat.lt_le_incl _ _ Hi)) n.
+ exfalso; rewrite <- H in H0; apply Nat.le_ngt with (sep__part_fun i (Nat.lt_le_incl _ _ Hi)) n.
   apply sep__part_fun_bnd.
  assumption.
 Qed.
@@ -877,7 +877,7 @@ Proof.
      unfold part_tot_nat_fun in |- *.
      elim (le_lt_dec n j); intro; simpl in |- *.
       exfalso.
-      apply le_not_lt with n j.
+      apply Nat.le_ngt with n j.
        assumption.
       apply Nat.lt_le_trans with (sep__part_fun (S i) Hi'').
        assumption.
@@ -885,13 +885,13 @@ Proof.
      apply mult_wd; algebra.
      apply cg_minus_wd; apply prf1; auto.
     exfalso.
-    apply le_not_lt with (sep__part_fun i Hi') j.
+    apply Nat.le_ngt with (sep__part_fun i Hi') j.
      assumption.
     cut (sep__part_fun i Hi' = sep__part_fun i (Nat.lt_le_incl _ _ Hi));
       [ intro | apply sep__part_fun_wd; auto ].
     rewrite H1; assumption.
    exfalso.
-   apply le_not_lt with (S j) (sep__part_fun (S i) Hi).
+   apply Nat.le_ngt with (S j) (sep__part_fun (S i) Hi).
     cut (sep__part_fun (S i) Hi = sep__part_fun (S i) Hi''); [ intro | apply sep__part_fun_wd; auto ].
     rewrite H1; apply H0.
    rewrite <- (Nat.lt_succ_pred (sep__part_fun i (Nat.lt_le_incl _ _ Hi)) (sep__part_fun (S i) Hi)) .
@@ -901,7 +901,7 @@ Proof.
  apply Sumx_wd; intros.
  unfold part_tot_nat_fun in |- *.
  elim (le_lt_dec n i); intro; simpl in |- *.
-  exfalso; apply le_not_lt with n i; auto.
+  exfalso; apply Nat.le_ngt with n i; auto.
  apply mult_wd; algebra.
  apply cg_minus_wd; apply prf1; auto.
 Qed.
@@ -996,7 +996,7 @@ Proof.
       apply Sumx_resp_leEq; intros.
       unfold part_tot_nat_fun in |- *.
       elim (le_lt_dec n i); intro; simpl in |- *.
-       exfalso; exact (le_not_lt _ _ a0 H).
+       exfalso; lia.
       unfold delta in |- *.
       apply leEq_transitive with ((M[+]M)[*] (alpha[/] _[//]
         mult_resp_ap_zero _ _ _ (nring_ap_zero _ _ SPap_n) (max_one_ap_zero M)) [/]TwoNZ).
@@ -1022,19 +1022,19 @@ Proof.
   intros; elim (le_lt_dec (sep__part_fun i (Nat.lt_le_incl _ _ Hi)) j); intro; simpl in |- *.
    elim (le_lt_dec j (pred (sep__part_fun (S i) Hi))); intro; simpl in |- *.
     elim (le_lt_dec n j); intro; simpl in |- *.
-     exfalso; apply (le_not_lt n j).
+     exfalso; apply (Nat.le_ngt n j).
       assumption.
      eapply Nat.lt_le_trans.
       apply H0.
      apply sep__part_fun_bnd.
     algebra.
-   exfalso; apply (le_not_lt _ _ H0).
+   exfalso; apply (proj1 (Nat.le_ngt _ _) H0).
    rewrite <- (Nat.lt_succ_pred (sep__part_fun i Hi') (sep__part_fun (S i) Hi'')).
     cut (sep__part_fun (S i) Hi'' = sep__part_fun (S i) Hi); [ intro | apply sep__part_fun_wd; auto ].
     rewrite H1; auto with arith.
    apply sep__part_fun_mon.
    apply Nat.lt_succ_diag_r.
-  exfalso; apply (le_not_lt _ _ H).
+  exfalso; apply (proj1 (Nat.le_ngt _ _) H).
   rewrite sep__part_fun_i.
    2: assumption.
   rewrite sep__part_fun_i in b0; assumption.
diff --git a/ftc/Taylor.v b/ftc/Taylor.v
index e7453860..ffda8c2e 100644
--- a/ftc/Taylor.v
+++ b/ftc/Taylor.v
@@ -112,7 +112,7 @@ Proof.
  clear H; intros. rename X into H.
  elim (cg_minus_strext _ _ _ _ _ H); clear H; intro H.
   unfold Taylor_Rem, Taylor_Seq', funct_i in H.
-  cut (Dom (FSumx n (fun i (Hi : i < n) => [-C-] (fi n Hf' (S i) (lt_n_S _ _ Hi) a Ha[/] _[//]
+  cut (Dom (FSumx n (fun i (Hi : i < n) => [-C-] (fi n Hf' (S i) (proj1 (Nat.succ_lt_mono _ _) Hi) a Ha[/] _[//]
     nring_fac_ap_zero IR (S i)) {*} (FId{-} [-C-]a) {^}S i)) b).
    2: apply FSumx_pred'; repeat split.
   intro H0.
@@ -121,7 +121,7 @@ Proof.
     apply pfstrx with (Hx := Hpred a Ha) (Hy := Hpred b Hb).
     apply ap_symmetric_unfolded; apply zero_minus_apart; auto.
    cut (ext_fun_seq' (fun i (Hi : i < n) => [-C-]
-     (fi n Hf' (S i) (lt_n_S _ _ Hi) a Ha[/] _[//]nring_fac_ap_zero IR (S i)) {*}
+     (fi n Hf' (S i) (proj1 (Nat.succ_lt_mono _ _) Hi) a Ha[/] _[//]nring_fac_ap_zero IR (S i)) {*}
        (FId{-} [-C-]a) {^}S i)).
     2: red in |- *; repeat split.
    intro H1.
@@ -134,7 +134,7 @@ Proof.
     2: exact (FSumx_char _ _ _ _ H1).
    simpl in H2.
    cut (nat_less_n_fun (fun i (Hi : i < n) =>
-     (fi n Hf' (S i) (lt_n_S _ _ Hi) a Ha[/] _[//]nring_fac_ap_zero IR (S i)) [*]
+     (fi n Hf' (S i) (proj1 (Nat.succ_lt_mono _ _) Hi) a Ha[/] _[//]nring_fac_ap_zero IR (S i)) [*]
        (nexp IR i (b[+][--]a) [*] (b[+][--]a)))); intros.
     cut (nat_less_n_fun (fun i (Hi : i < n) => ([0]:IR))); intros.
      elim (Sumx_strext _ _ _ _ H3 H4 H2); clear H H0 H1 H2 H3 H4; intros N HN.
@@ -163,7 +163,7 @@ Proof.
      algebra.
     exact (FSumx_char _ _ _ _ H1).
    cut (ext_fun_seq' (fun i (Hi : i < n) => [-C-]
-     (fi n Hf' (S i) (lt_n_S _ _ Hi) a Ha[/] _[//]nring_fac_ap_zero IR (S i)) {*}
+     (fi n Hf' (S i) (proj1 (Nat.succ_lt_mono _ _) Hi) a Ha[/] _[//]nring_fac_ap_zero IR (S i)) {*}
        (FId{-} [-C-]a) {^}S i)). intro H2.
     apply eq_transitive_unfolded with (Part _ _ (Hpred b Hb) [-]Part _ _ (Hpred a Ha) [-] Sumx
       (fun i (Hi : i < n) => Part _ _ (FSumx_pred _ _ H2 b H0 i Hi))).
diff --git a/ftc/TaylorLemma.v b/ftc/TaylorLemma.v
index 5ad1ba5e..2db43478 100644
--- a/ftc/TaylorLemma.v
+++ b/ftc/TaylorLemma.v
@@ -414,15 +414,15 @@ Qed.
 
 Transparent funct_i' FSumx.
 
-Let funct_aux n Hf i Hi := PartInt (fi (S n) Hf (S i) (lt_n_S _ _ Hi)) {*}
+Let funct_aux n Hf i Hi := PartInt (fi (S n) Hf (S i) (proj1 (Nat.succ_lt_mono _ _) Hi)) {*}
   [-C-] ([1][/] _[//]nring_fac_ap_zero IR i) {*} ( [-C-]b{-}FId) {^}i.
 
 Lemma Taylor_lemma6 :  forall n Hf Hf' i Hi, Derivative_I Hab'
- (PartInt (fi n Hf i Hi)) (PartInt (fi (S n) Hf' (S i) (lt_n_S _ _ Hi))).
+ (PartInt (fi n Hf i Hi)) (PartInt (fi (S n) Hf' (S i) (proj1 (Nat.succ_lt_mono _ _) Hi))).
 Proof.
  intros.
  cut (Derivative_I_n Hab' 1 (PartInt (fi n Hf i Hi))
-   (PartInt (fi (S n) Hf' (S i) (lt_n_S i (S n) Hi)))).
+   (PartInt (fi (S n) Hf' (S i) (proj1 (Nat.succ_lt_mono i (S n)) Hi)))).
   intro H.
   simpl in H.
   elim H; intros f' H1 H2.
@@ -474,7 +474,7 @@ Proof.
  set (p := pred i) in *; clearbody p; clear Hi i.
  intros.
  cut (Derivative_I Hab' (PartInt (fi n Hf _ Hi'))
-   (PartInt (fi (S n) Hf' (S (S p)) (lt_n_S _ _ Hi')))); [ intro | apply Taylor_lemma6 ].
+   (PartInt (fi (S n) Hf' (S (S p)) (proj1 (Nat.succ_lt_mono _ _) Hi')))); [ intro | apply Taylor_lemma6 ].
  unfold funct_aux, funct_i' in |- *.
  New_Deriv.
   apply Feq_reflexive.
@@ -485,7 +485,7 @@ Proof.
  intros x X0 Hx Hx'.
  simpl in Hx, Hx'; simpl in |- *.
  set (fiSp1 := fi n Hf (S p) Hi') in *.
- set (fiSp2 := fi (S n) Hf' (S p) (lt_n_S p (S n) (lt_5 (S p) (S n) Hi'))) in *.
+ set (fiSp2 := fi (S n) Hf' (S p) (proj1 (Nat.succ_lt_mono p (S n)) (lt_5 (S p) (S n) Hi'))) in *.
  cut (forall x y : subset I, scs_elem _ _ x [=] scs_elem _ _ y -> fiSp1 x [=] fiSp2 y); intros.
   set (x1 := Build_subcsetoid_crr IR _ _ (ProjIR1 (ProjIR1 (ProjIR1 Hx)))) in *.
   simpl in (value of x1); fold x1 in |- *.
@@ -497,7 +497,7 @@ Proof.
   simpl in (value of x4); fold x4 in |- *.
   set (x5 := Build_subcsetoid_crr IR _ _ (ProjIR1 (ProjIR2 (ProjIR1 (ProjIR2 Hx))))) in *.
   simpl in (value of x5); fold x5 in |- *.
-  set (fiSSp := fi (S n) Hf' (S (S p)) (lt_n_S (S p) (S n) Hi')) in *.
+  set (fiSSp := fi (S n) Hf' (S (S p)) (proj1 (Nat.succ_lt_mono (S p) (S n)) Hi')) in *.
   set (pp := [1][/] nring (fact p + p * fact p) [//]nring_fac_ap_zero IR (S p)) in *.
   set (bxp := nexp _ p (b[-]x)) in *.
   set (a1 := fiSp1 x1) in *; set (a5 := fiSSp x5) in *;
@@ -521,7 +521,7 @@ Proof.
   transitivity (S p * fact p); auto with arith.
  unfold fiSp1, fiSp2 in |- *.
  apply eq_transitive_unfolded with (PartInt (fi n Hf (S p) Hi') (scs_elem _ _ x0) (scs_prf _ _ x0)).
-  2: apply eq_transitive_unfolded with (PartInt (fi (S n) Hf' (S p) (lt_n_S _ _ (lt_5 _ _ Hi')))
+  2: apply eq_transitive_unfolded with (PartInt (fi (S n) Hf' (S p) (proj1 (Nat.succ_lt_mono _ _) (lt_5 _ _ Hi')))
     (scs_elem _ _ x0) (scs_prf _ _ x0)).
    simpl in |- *; apply csf_wd_unfolded.
    case x0; simpl in |- *; algebra.
@@ -536,7 +536,7 @@ Lemma Taylor_lemma8 : forall n Hf Hf' Hi,
   Derivative_I Hab' (funct_i' n Hf 0 Hi) (funct_aux n Hf' 0 Hi).
 Proof.
  intros.
- cut (Derivative_I Hab' (PartInt (fi n Hf _ Hi)) (PartInt (fi (S n) Hf' 1 (lt_n_S _ _ Hi))));
+ cut (Derivative_I Hab' (PartInt (fi n Hf _ Hi)) (PartInt (fi (S n) Hf' 1 (proj1 (Nat.succ_lt_mono _ _) Hi))));
    [ intro | apply Taylor_lemma6 ].
  unfold funct_aux, funct_i' in |- *; New_Deriv.
   apply Feq_reflexive; Lazy_Included.
@@ -544,7 +544,7 @@ Proof.
    Lazy_Included.
   Lazy_Included.
  intros; simpl in |- *.
- apply eq_transitive_unfolded with (fi (S n) Hf' 1 (lt_n_S _ _ Hi)
+ apply eq_transitive_unfolded with (fi (S n) Hf' 1 (proj1 (Nat.succ_lt_mono _ _) Hi)
    (Build_subcsetoid_crr _ _ _ (ProjIR1 (ProjIR2 (ProjIR1 (ProjIR2 Hx))))) [*]
      ([1][/] _[//]nring_fac_ap_zero IR 0) [*][1]).
   simpl in |- *; rational.
@@ -630,9 +630,9 @@ Proof.
     repeat (split; auto).
    intros x H2 Hx Hx'; simpl in |- *.
    repeat apply mult_wdl.
-   apply eq_transitive_unfolded with (PartInt (fi (S n) Hf (S n) (lt_n_S _ _ (Nat.lt_succ_diag_r _))) x H2).
+   apply eq_transitive_unfolded with (PartInt (fi (S n) Hf (S n) (proj1 (Nat.succ_lt_mono _ _) (Nat.lt_succ_diag_r _))) x H2).
     2: apply eq_transitive_unfolded with (PartInt
-      (fi (S (S n)) Hf' (S n) (lt_n_S _ _ (lt_5 _ _ (Nat.lt_succ_diag_r (S n))))) x H2).
+      (fi (S (S n)) Hf' (S n) (proj1 (Nat.succ_lt_mono _ _) (lt_5 _ _ (Nat.lt_succ_diag_r (S n))))) x H2).
      simpl in |- *; apply csf_wd_unfolded; simpl in |- *; algebra.
     2: simpl in |- *; apply csf_wd_unfolded; simpl in |- *; algebra.
    apply Feq_imp_eq with (Compact Hab).
@@ -808,7 +808,7 @@ Proof.
       ([1][/] _[//]nring_fac_ap_zero _ n) [*] (b[-]c) [^]n).
      repeat apply mult_wdl; apply pfwdef; algebra.
     repeat apply mult_wdl.
-    apply eq_transitive_unfolded with (PartInt (fi (S n) Hf' (S n) (lt_n_S _ _ (Nat.lt_succ_diag_r _))) c Hc').
+    apply eq_transitive_unfolded with (PartInt (fi (S n) Hf' (S n) (proj1 (Nat.succ_lt_mono _ _) (Nat.lt_succ_diag_r _))) c Hc').
      2: simpl in |- *; apply csf_wd_unfolded; simpl in |- *; algebra.
     apply Feq_imp_eq with (Compact Hab).
      unfold Hab in |- *; apply Derivative_I_n_unique with (S n) F.
diff --git a/liouville/CPoly_Euclid.v b/liouville/CPoly_Euclid.v
index d79cec1d..99fb9872 100644
--- a/liouville/CPoly_Euclid.v
+++ b/liouville/CPoly_Euclid.v
@@ -104,7 +104,7 @@ Proof.
   destruct m; [ rewrite -> (nth_coeff_wd _ _ _ _ (s0 H1)); reflexivity | apply (d m H1); apply le_n ].
  apply (IHn (S m) _ ([0] [+X*] b) (c [-] _C_ s [*] b)); [ | | | rewrite <- H2, cpoly_lin, <- c_zero; unfold cg_minus; ring ].
    unfold degree_le; intros; rewrite <- (coeff_Sm_lin _ _ s).
-   apply H; apply lt_n_S; apply H3.
+   apply H; apply -> Nat.succ_lt_mono; apply H3.
   split; [ rewrite -> coeff_Sm_lin; destruct H0; apply H0 | unfold degree_le; intros ].
   destruct m0; [ inversion H3 | simpl; destruct H0 ].
   apply H4; apply lt_S_n; apply H3.
@@ -145,7 +145,7 @@ Proof.
   split.
    intros; unfold degree_le; intros; apply y0; apply Nat.le_lt_trans with n0; [ | assumption ].
    unfold degree_le in H1; apply not_gt; intro; unfold gt in H3.
-   set (tmp := (H1 (S n) (lt_n_S _ _ H3))); rewrite -> H in tmp.
+   set (tmp := (H1 (S n) (proj1 (Nat.succ_lt_mono _ _) H3))); rewrite -> H in tmp.
    apply (eq_imp_not_ap _ _ _ tmp); apply ring_non_triv.
   intro; unfold degree_le in H1; rewrite -> H1 in H; [ | apply Nat.lt_0_succ ].
   destruct (eq_imp_not_ap _ _ _ H); apply ap_symmetric; apply ring_non_triv.
diff --git a/logic/CLogic.v b/logic/CLogic.v
index e4a0308b..9aaa23fd 100644
--- a/logic/CLogic.v
+++ b/logic/CLogic.v
@@ -454,7 +454,7 @@ Proof.
  elim (gt_eq_gt_dec p q); intro H0.
   elim H0; auto.
  exfalso.
- apply lt_not_le with q p; auto.
+ apply Nat.lt_nge with q p; auto.
 Qed.
 
 Lemma Cnat_total_order : forall m n : nat, m <> n -> {m < n} + {n < m}.
diff --git a/reals/Bridges_LUB.v b/reals/Bridges_LUB.v
index 0fb2082e..f97a8c83 100644
--- a/reals/Bridges_LUB.v
+++ b/reals/Bridges_LUB.v
@@ -852,7 +852,7 @@ Proof.
      apply very_weak_binomial.
       apply recip_resp_pos.
       apply pos_nring_S.
-     apply lt_n_S.
+     apply -> Nat.succ_lt_mono.
      apply neq_O_lt.
      apply (nring_ap_zero_imp R1).
      apply Greater_imp_ap.
diff --git a/reals/CReals1.v b/reals/CReals1.v
index b9c6cc08..87da318d 100644
--- a/reals/CReals1.v
+++ b/reals/CReals1.v
@@ -248,7 +248,7 @@ Proof.
   intro; apply not_ge; auto.
  intro.
  cut (f n <= f m).
-  apply lt_not_le; auto.
+  apply Nat.lt_nge; auto.
  apply monF; assumption.
 Qed.
 (* end hide *)
diff --git a/reals/NRootIR.v b/reals/NRootIR.v
index 6be578c5..2f13775b 100644
--- a/reals/NRootIR.v
+++ b/reals/NRootIR.v
@@ -684,9 +684,9 @@ Proof.
   assumption.
  intros.
  elim (le_lt_dec m i); intro;
-   [ simpl in |- * | exfalso; apply (le_not_lt m i); auto with arith ].
+   [ simpl in |- * | exfalso; apply (Nat.le_ngt m i); auto with arith ].
  elim (le_lt_dec i n); intro;
-   [ simpl in |- * | exfalso; apply (le_not_lt i n); auto with arith ].
+   [ simpl in |- * | exfalso; apply (Nat.le_ngt i n); auto with arith ].
  algebra.
 Qed.
 
diff --git a/reals/Q_dense.v b/reals/Q_dense.v
index 7ae1cf31..24f9cc76 100644
--- a/reals/Q_dense.v
+++ b/reals/Q_dense.v
@@ -868,7 +868,7 @@ Proof.
     rstepr ((start_r x[-]start_l x)[*]nring (S (S (N + 3)))).
     apply mult_resp_less_lft.
      apply nring_less.
-     apply lt_n_S.
+     apply -> Nat.succ_lt_mono.
      apply le_lt_n_Sm.
      apply Nat.le_add_r.
     apply shift_zero_less_minus.
diff --git a/reals/fast/CRcorrect.v b/reals/fast/CRcorrect.v
index 222471fe..7d7c2718 100644
--- a/reals/fast/CRcorrect.v
+++ b/reals/fast/CRcorrect.v
@@ -823,7 +823,7 @@ Proof.
  clear Hc.
  unfold y.
  destruct (lt_le_dec m a) as [Z|Z].
-  elim (le_not_lt _ _ Z).
+  elim (proj1 (Nat.le_ngt _ _) Z).
   unfold m.
   apply Nat.lt_le_trans with (S (Nat.max a n)); auto with *.
  change (AbsSmall (proj1_sig e) (/ Qmax (proj1_sig z) (x b)-1 * / x m))%Q.
diff --git a/reals/stdlib/CMTProductIntegral.v b/reals/stdlib/CMTProductIntegral.v
index 9e757e79..c171e4e9 100644
--- a/reals/stdlib/CMTProductIntegral.v
+++ b/reals/stdlib/CMTProductIntegral.v
@@ -666,11 +666,11 @@ Proof.
   destruct b. destruct b0. exact (ndiff eq_refl). contradiction.
   destruct b0. contradiction. exact (ndiff eq_refl).
   rewrite nth_error_None, <- H in des0.
-  exact (lt_not_le _ _ nlen des0).
+  exact (proj1 (Nat.lt_nge _ _) nlen des0).
   rewrite nth_error_None in desl.
-  exact (lt_not_le _ _ nlen desl).
+  exact (proj1 (Nat.lt_nge _ _) nlen desl).
   rewrite nth_error_None, <- H0 in des.
-  exact (lt_not_le _ _ nlen des).
+  exact (proj1 (Nat.lt_nge _ _) nlen des).
 Qed.
 
 Definition ProdIntegrableSimplify
@@ -1122,12 +1122,12 @@ Proof.
       rewrite nth_list_prod in des2. unfold fst in des2.
       rewrite (FreeSubsetsLength
                  (length hn) (nth (nl / length (FreeSubsets (length hn))) (FreeSubsets (length hn)) nil)) in des2.
-      exact (lt_not_le _ _ H0 des2).
+      exact (proj1 (Nat.lt_nge _ _) H0 des2).
       apply nth_In.
       apply Nat.div_lt_upper_bound in H1. exact H1.
       intro abs. rewrite abs in flen. inversion flen. exact H1.
       exfalso. apply nth_error_None in des. rewrite map_length in des.
-      exact (lt_not_le _ _ H0 des).
+      exact (proj1 (Nat.lt_nge _ _) H0 des).
     + assert (Forall (fun h => ~h x) (map prodint_f hn)).
       { apply SubsetIntersectFilterOut. intros.
         destruct (FreeSubsetsFull filter) as [n [H2 H3]].
@@ -1180,11 +1180,11 @@ Proof.
       rewrite nth_list_prod in des2. unfold snd in des2.
       rewrite (FreeSubsetsLength
                  (length hn) (nth (nl mod length (FreeSubsets (length hn))) (FreeSubsets (length hn)) nil)) in des2.
-      exact (lt_not_le _ _ H0 des2).
+      exact (proj1 (Nat.lt_nge _ _) H0 des2).
       apply nth_In. apply Nat.mod_bound_pos. apply Nat.le_0_l.
       exact flen. exact H1.
       exfalso. apply nth_error_None in des. rewrite map_length in des.
-      exact (lt_not_le _ _ H0 des).
+      exact (proj1 (Nat.lt_nge _ _) H0 des).
     + assert (Forall (fun h => ~h y) (map prodint_g hn)).
       { apply SubsetIntersectFilterOut. intros.
         destruct (FreeSubsetsFull filter) as [n [H2 H3]].
diff --git a/reals/stdlib/CMTprofile.v b/reals/stdlib/CMTprofile.v
index c6aba9d5..4ee62404 100644
--- a/reals/stdlib/CMTprofile.v
+++ b/reals/stdlib/CMTprofile.v
@@ -40,6 +40,7 @@ Require Import CMTIntegrableFunctions.
 Require Import CMTIntegrableSets.
 Require Import CMTFullSets.
 Require Import CMTReals.
+Require Import Lia.
 
 Local Open Scope ConstructiveReals.
 
@@ -984,7 +985,7 @@ Proof.
       apply (CRle_trans _ b). apply BinarySubdivInside.
       apply CRlt_asym, ltab. apply le_S_n, l0. apply CRlt_asym, (snd beta).
       exfalso. pose proof (Nat.lt_le_trans _ _ _ l l0).
-      apply (lt_not_le _ _ H0). apply le_S, Nat.le_refl.
+      apply (proj1 (Nat.lt_nge _ _) H0). apply le_S, Nat.le_refl.
       apply StepApproxIntegralIncr.
       apply CRlt_asym, BinarySubdivIncr. exact (pair aPos ltab).
       apply CRlt_asym, BinarySubdivIncr. exact (pair aPos ltab).
@@ -1023,7 +1024,7 @@ Proof.
     + exfalso. apply le_S_n in l0.
       apply (Nat.le_trans _ _ _ H) in l0. clear H.
       apply (Nat.mul_le_mono_pos_l _ _ 2) in l0.
-      apply (Nat.le_trans _ _ _ l) in l0. apply (le_not_lt _ _ l0 (Nat.le_refl _)).
+      apply (Nat.le_trans _ _ _ l) in l0. apply (proj1 (Nat.le_ngt _ _) l0 (Nat.le_refl _)).
       apply le_n_S, Nat.le_0_l.
     + apply StepApproxIntegralIncr.
       apply BinarySubdivInside. apply CRlt_asym, ltab.
@@ -1098,7 +1099,7 @@ Proof.
       apply le_S_n, l0. apply CRlt_asym, (snd beta).
     + exfalso. apply le_S_n in l0. apply le_S_n in l.
       apply (Nat.le_trans _ _ (2^S n)) in H.
-      apply (Nat.le_trans _ _ _ H) in l0. apply (le_not_lt _ _ l0).
+      apply (Nat.le_trans _ _ _ H) in l0. apply (proj1 (Nat.le_ngt _ _) l0).
       apply le_S, Nat.le_refl. apply Nat.mul_le_mono_nonneg_l.
       apply Nat.le_0_l. exact l.
     + clear l l0.
@@ -1339,7 +1340,7 @@ Proof.
     unfold StepApproxDiscretize in c0.
     destruct (2^n)%nat eqn:des. apply Nat.le_0_l. rewrite <- des.
     destruct (le_lt_dec (S (S n0)) (S n0)). exfalso.
-    exact (le_not_lt _ _ l0 (Nat.le_refl _)).
+    lia.
     destruct (le_lt_dec (S (S n0)) (S i)).
     + apply le_S_n in l1. pose proof (Nat.le_antisymm _ _ l l1).
       subst i. rewrite <- des. apply Nat.le_refl.
@@ -1365,7 +1366,7 @@ Proof.
     apply (CRlt_trans _ _ _ H) in c0. unfold StepApproxDiscretize in c0.
     destruct j. apply Nat.le_0_l.
     destruct (le_lt_dec (S (2 ^ n)) (S j)).
-    exfalso. apply le_S_n in l1. exact (le_not_lt _ _ l1 l0).
+    exfalso. apply le_S_n in l1. lia.
     destruct (le_lt_dec (S (2 ^ n)) (S i)).
     apply le_S_n in l1. apply le_S_n in l2. exact (Nat.le_trans _ _ _ l1 l2).
     destruct (le_lt_dec (S j) i). exact l3. exfalso.
@@ -1625,7 +1626,7 @@ Proof.
                  (CRlt_trans 0 a b aPos ltab, right_ordered ext)
                  (IntExtRightPos ext (CRlt_asym a b ltab), right_ordered ext) ).
       apply CRlt_asym, c1.
-      exfalso; exact (lt_not_le _ _ l0 (Nat.le_refl _)). }
+      exfalso; exact (proj1 (Nat.lt_nge _ _) l0 (Nat.le_refl _)). }
   assert (forall k : nat, sk k <= sk (S k)) as skIncr.
   { unfold sk. intros k. destruct k.
     - destruct (H3 O).
@@ -1713,7 +1714,7 @@ Proof.
       apply (CRlt_trans _ _ _ H4), (CRlt_trans _ _ _ (snd ltxy)).
       apply (CRle_lt_trans _ _ _ H5), (snd ltuv).
       destruct (le_lt_dec (S (2 ^ m)) (S x0)).
-      exfalso. apply le_S_n in l0. exact (lt_not_le _ _ l l0).
+      exfalso. apply le_S_n in l0. exact (proj1 (Nat.lt_nge _ _) l l0).
       assert (v <= BinarySubdiv a b m x0).
       { apply (CRle_trans _ (BinarySubdiv a b m (S x0) +
                              CRpow (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) m * - (b - a))).
@@ -1805,7 +1806,7 @@ Proof.
         apply CRlt_asym, (snd ltuv).
         destruct (le_lt_dec (S (2 ^ max n m)) (S x0)).
         apply le_S_n in l0.
-        exfalso. exact (lt_not_le _ _ l l0).
+        exfalso. exact (proj1 (Nat.lt_nge _ _) l l0).
         apply CRlt_asym in mcv.
         rewrite <- BinarySubdivNext, CRplus_assoc, CRplus_opp_r, CRplus_0_r in mcv.
         apply StepApproxIntegralIncr.
diff --git a/reals/stdlib/ConstructiveCauchyIntegral.v b/reals/stdlib/ConstructiveCauchyIntegral.v
index c197a8c2..7315844c 100644
--- a/reals/stdlib/ConstructiveCauchyIntegral.v
+++ b/reals/stdlib/ConstructiveCauchyIntegral.v
@@ -371,7 +371,7 @@ Proof.
       rewrite Nat.add_comm. apply Nat.lt_add_lt_sub_l. exact H5.
       intro abs.
       destruct H2, H6. specialize (H6 n (S n) (Nat.le_refl _)).
-      apply Nat.sub_0_le in abs. apply (le_not_lt _ _ abs).
+      apply Nat.sub_0_le in abs. apply (proj1 (Nat.le_ngt _ _) abs).
       apply H6, le_n_S, H4. apply H2. apply le_n_S, H4.
       apply (CRle_trans
                _ (CRsum
@@ -391,7 +391,7 @@ Proof.
       apply H2, le_n_S, H4.
       intro abs.
       destruct H2, H6. specialize (H6 n (S n) (Nat.le_refl _)).
-      apply Nat.sub_0_le in abs. apply (le_not_lt _ _ abs).
+      apply Nat.sub_0_le in abs. apply (proj1 (Nat.le_ngt _ _) abs).
       apply H6, le_n_S, H4.
       destruct H. apply CRlt_asym. apply (c0 eps _ _ epsPos).
       apply (CRle_lt_trans _ (PartitionMesh (ipt_seq P) (S (ipt_last P)))).
@@ -402,13 +402,13 @@ Proof.
       apply Nat.add_le_mono_r. apply Nat.le_0_l.
       intro abs.
       destruct H2, H2. specialize (H2 n (S n) (Nat.le_refl _)).
-      apply Nat.sub_0_le in abs. apply (le_not_lt _ _ abs).
+      apply Nat.sub_0_le in abs. apply (proj1 (Nat.le_ngt _ _) abs).
       apply H2. apply le_n_S, H4.
       rewrite Nat.add_comm. apply Nat.lt_add_lt_sub_l.
       apply le_n_S in H5. rewrite Nat.succ_pred in H5. exact H5.
       intro abs.
       destruct H2, H2. specialize (H2 n (S n) (Nat.le_refl _)).
-      apply Nat.sub_0_le in abs. apply (le_not_lt _ _ abs).
+      apply Nat.sub_0_le in abs. apply (proj1 (Nat.le_ngt _ _) abs).
       apply H2. apply le_n_S, H4.
       rewrite sum_scale, CRmult_comm. apply CRmult_le_compat_l.
       apply CRlt_asym, epsPos.
@@ -427,7 +427,7 @@ Proof.
       intro abs.
       destruct H2, H5.
       specialize (H5 n (S n) (Nat.le_refl _)).
-      apply Nat.sub_0_le in abs. apply (le_not_lt _ _ abs), H5, le_n_S, H4.
+      apply Nat.sub_0_le in abs. apply (proj1 (Nat.le_ngt _ _) abs), H5, le_n_S, H4.
     + rewrite (CRsum_eq _  (fun k : nat => (ipt_seq P (S k) - ipt_seq P k) * eps)).
       rewrite sum_scale, CRmult_comm. apply CRmult_le_compat_l.
       apply CRlt_asym, epsPos.
@@ -451,7 +451,7 @@ Proof.
       intro abs.
       destruct H2, H5.
       specialize (H5 i (S i) (Nat.le_refl _)).
-      apply Nat.sub_0_le in abs. apply (le_not_lt _ _ abs), H5, le_n_S, H4.
+      apply Nat.sub_0_le in abs. apply (proj1 (Nat.le_ngt _ _) abs), H5, le_n_S, H4.
     + unfold IntegralFiniteSum.
       rewrite partition_sum_by_packets. reflexivity. exact H2.
 Qed.
@@ -1171,7 +1171,7 @@ Proof.
   - apply P.
   - unfold ConcatSequences.
     destruct (lt_dec (S (S (ipt_last P) + ipt_last Q)) (S (ipt_last P))).
-    + exfalso. apply (lt_not_le _ _ l), le_n_S, (Nat.le_trans _ (S (ipt_last P) + 0)).
+    + exfalso. apply (proj1 (Nat.lt_nge _ _) l), le_n_S, (Nat.le_trans _ (S (ipt_last P) + 0)).
       rewrite Nat.add_0_r. apply le_S, Nat.le_refl. apply Nat.add_le_mono_l, Nat.le_0_l.
     + replace (S (S (ipt_last P) + ipt_last Q) - (S (ipt_last P)))%nat
         with (S (ipt_last Q)).
@@ -1226,12 +1226,12 @@ Proof.
     + apply Nat.le_antisymm. apply le_S_n, Nat.nlt_ge, n. exact H.
   - apply CRsum_eq. intros. unfold ConcatSequences.
     destruct (lt_dec (S ipt_last0 + i) (S ipt_last0)).
-    exfalso. apply (lt_not_le _ _ l).
+    exfalso. apply (proj1 (Nat.lt_nge _ _) l).
     apply (Nat.le_trans _ (S ipt_last0 + 0)).
     rewrite Nat.add_0_r. apply Nat.le_refl. apply Nat.add_le_mono_l, Nat.le_0_l.
     clear n.
     destruct (lt_dec (S (S ipt_last0 + i)) (S ipt_last0)).
-    exfalso. apply lt_not_le in l. apply l, le_n_S.
+    exfalso. apply Nat.lt_nge in l. apply l, le_n_S.
     apply (Nat.le_trans _ (S ipt_last0 + 0)).
     rewrite Nat.add_0_r. apply le_S, Nat.le_refl. apply Nat.add_le_mono_l, Nat.le_0_l.
     clear n.
@@ -1280,10 +1280,10 @@ Proof.
       setoid_replace (ConcatSequences xn yn n (S (n + p)) - ConcatSequences xn yn n (n+p))
         with (yn (S p) - yn p).
       apply H0. unfold ConcatSequences.
-      destruct (lt_dec (S (n + p)) n). exfalso. apply (lt_not_le _ _ l).
+      destruct (lt_dec (S (n + p)) n). exfalso. apply (proj1 (Nat.lt_nge _ _) l).
       apply (Nat.le_trans _ (S n + 0)). rewrite Nat.add_0_r. apply le_S, Nat.le_refl.
       simpl. apply le_n_S, Nat.add_le_mono_l, Nat.le_0_l.
-      clear n0. destruct (lt_dec (n + p) n). exfalso. apply (lt_not_le _ _ l).
+      clear n0. destruct (lt_dec (n + p) n). exfalso. apply (proj1 (Nat.lt_nge _ _) l).
       apply (Nat.le_trans _ (n + 0)). rewrite Nat.add_0_r. apply Nat.le_refl.
       apply Nat.add_le_mono_l, Nat.le_0_l. clear n0.
       rewrite (Nat.add_comm n), Nat.add_sub. apply CRplus_morph.
@@ -1384,12 +1384,12 @@ Proof.
       rewrite (Nat.sub_succ_r _ (S ipt_last0)).
       rewrite Nat.succ_pred. reflexivity.
       intro abs. apply Nat.sub_0_le in abs.
-      exact (lt_not_le _ _ H4 abs).
+      exact (proj1 (Nat.lt_nge _ _) H4 abs).
       rewrite (Nat.sub_succ_r _ (S ipt_last0)).
       rewrite Nat.succ_pred.
       rewrite Nat.le_sub_le_add_l, Nat.add_succ_r. exact H3.
       intro abs. apply Nat.sub_0_le in abs.
-      exact (lt_not_le _ _ H4 abs).
+      exact (proj1 (Nat.lt_nge _ _) H4 abs).
 Qed.
 
 Lemma FunLocSorted : forall (xn : list Q),
diff --git a/reals/stdlib/ConstructiveDiagonal.v b/reals/stdlib/ConstructiveDiagonal.v
index 1044152b..840c8dcb 100644
--- a/reals/stdlib/ConstructiveDiagonal.v
+++ b/reals/stdlib/ConstructiveDiagonal.v
@@ -57,12 +57,12 @@ Proof.
   intros. generalize dependent n. induction k.
   - simpl. split.
     + intro. destruct (Nat.eq_dec (proj1_sig un O) n).
-      assumption. exfalso. apply (lt_not_le n (S n)).
+      assumption. exfalso. apply (Nat.lt_nge n (S n)).
       apply Nat.le_refl. assumption.
     + intro. destruct (Nat.eq_dec (proj1_sig un O) n). apply Nat.le_0_l.
       exfalso. pose proof (SubSeqAboveId un n).
       destruct un. simpl in H. simpl in n0. simpl in H0.
-      apply (lt_not_le (x n) (x (S n))). apply l. apply Nat.le_refl.
+      apply (Nat.lt_nge (x n) (x (S n))). apply l. apply Nat.le_refl.
       rewrite H. assumption.
   - split.
     + intro. simpl. simpl in H.
@@ -87,7 +87,7 @@ Proof.
     + intros. intro absurd. simpl in H.
       destruct (Nat.eq_dec (proj1_sig un (S k)) n).
       inversion H. subst k. pose proof (SubSeqAboveId un (S n)).
-      rewrite e in H1. apply (lt_not_le n (S n)). apply Nat.le_refl.
+      rewrite e in H1. apply (Nat.lt_nge n (S n)). apply Nat.le_refl.
       assumption. apply Nat.le_succ_r in H0. destruct H0.
       specialize (IHk n) as [IHk _].
       specialize (IHk H p H0). contradiction. subst p. contradiction.
@@ -104,7 +104,7 @@ Proof.
   - simpl. destruct (Nat.eq_dec (proj1_sig un O) (proj1_sig un O)). reflexivity.
     exfalso. exact (n (eq_refl _)).
   - simpl. destruct (Nat.eq_dec (proj1_sig un (S n)) (proj1_sig un O)).
-    exfalso. destruct un. simpl in e. apply (lt_not_le (x O) (x (S n))).
+    exfalso. destruct un. simpl in e. apply (Nat.lt_nge (x O) (x (S n))).
     apply l. apply le_n_S. apply Nat.le_0_l. rewrite e. apply Nat.le_refl.
     apply IHn.
 Qed.
@@ -139,7 +139,7 @@ Proof.
     destruct (Nat.eq_dec (SubSeqInv sub k k) (S k)). reflexivity.
     exfalso. apply n. clear n. apply SubSeqInvNotFound. intros.
     intro absurd. destruct p. rewrite absurd in H. exact (Nat.lt_irrefl k H).
-    destruct sub. simpl in absurd, H. apply (lt_not_le (x O) (x (S p))).
+    destruct sub. simpl in absurd, H. apply (Nat.lt_nge (x O) (x (S p))).
     apply l. apply le_n_S. apply Nat.le_0_l. rewrite absurd. apply le_S in H.
     apply le_S_n in H. apply H.
   - unfold FillSubSeqWithZeros.
@@ -172,10 +172,10 @@ Proof.
     destruct (Nat.lt_trichotomy p (S n)).
     apply Nat.le_succ_r in H2. destruct H2.
     specialize (inc p n H2). rewrite absurd in inc.
-    apply (lt_not_le (S (sub n + k)) (sub n)). assumption.
+    apply (Nat.lt_nge (S (sub n + k)) (sub n)). assumption.
     apply le_S. rewrite <- (Nat.add_0_r (sub n)). rewrite <- Nat.add_assoc.
     apply Nat.add_le_mono_l. apply Nat.le_0_l. inversion H2. subst p.
-    apply (lt_not_le (sub n) (S (sub n + k))). apply le_n_S.
+    apply (Nat.lt_nge (sub n) (S (sub n + k))). apply le_n_S.
     rewrite <- (Nat.add_0_r (sub n)). rewrite <- Nat.add_assoc.
     apply Nat.add_le_mono_l. apply Nat.le_0_l. rewrite <- absurd. apply Nat.le_refl.
     destruct H2. subst p. exact (Nat.lt_irrefl (sub (S n)) H1).
diff --git a/reals/stdlib/ConstructiveUniformCont.v b/reals/stdlib/ConstructiveUniformCont.v
index d6ca0322..942aced1 100644
--- a/reals/stdlib/ConstructiveUniformCont.v
+++ b/reals/stdlib/ConstructiveUniformCont.v
@@ -417,9 +417,9 @@ Proof.
     rewrite IHn.
     destruct (Pn (S (S n)) - Pn (S n))%nat eqn:des.
     exfalso. apply Nat.sub_0_le in des.
-    apply (le_not_lt _ _ des). apply H, Nat.le_refl. simpl.
+    apply (proj1 (Nat.le_ngt _ _) des). apply H, Nat.le_refl. simpl.
     pose proof (H n). destruct (Pn (S n)).
-    exfalso. apply (le_not_lt 0 (Pn n) (Nat.le_0_l _)). apply H1, le_S, Nat.le_refl.
+    exfalso. apply (proj1 (Nat.le_ngt 0 (Pn n)) (Nat.le_0_l _)). apply H1, le_S, Nat.le_refl.
     clear H1. simpl.
     rewrite (CRsum_eq (fun k : nat => xn (k + S n1)%nat)
                       (fun k : nat => xn (S n1 + k)%nat)).