diff --git a/Lebesgue/FinBij.v b/Lebesgue/FinBij.v
index ec01c18ecef9cc404a0ac67e30d737668133e08e..77694d0c0847749db24acdb42c484ff1f308e736 100644
--- a/Lebesgue/FinBij.v
+++ b/Lebesgue/FinBij.v
@@ -176,8 +176,8 @@ apply Nat.div_lt_upper_bound; [lia | easy].
 (* *)
 intros nm [Hn Hm]; unfold psi, prod_Pl.
 rewrite Nat.lt_succ_r in Hn, Hm; rewrite lt_mul_S, pred_mul_S, Nat.lt_succ_r.
-apply plus_le_compat; try easy.
-now apply mult_le_compat_l.
+apply Nat.add_le_mono; try easy.
+now apply Nat.mul_le_mono_l.
 (* *)
 intros p Hp; unfold phi, psi.
 rewrite (Nat.div_mod p (S N)) at 5; simpl; lia.
diff --git a/Lebesgue/LF_subcover.v b/Lebesgue/LF_subcover.v
index b09573694cb637d0ef2811b0625c4bb81bba5391..3573b1a210cee17769794ed174e12c718af22079 100644
--- a/Lebesgue/LF_subcover.v
+++ b/Lebesgue/LF_subcover.v
@@ -359,7 +359,7 @@ Qed.
 Lemma subcover_length : (q <= N)%nat.
 Proof.
 apply le_S_n.
-unfold q; rewrite <- S_pred_pos.
+unfold q; rewrite Nat.succ_pred_pos.
 apply LF_length.
 simpl; apply Nat.lt_0_succ.
 Qed.
diff --git a/Lebesgue/LInt_p.v b/Lebesgue/LInt_p.v
index 9273c77d685956c6bcd391e14015fd413797ebd7..22233a77e5ba613c803fe0726e5b08c908e21acf 100644
--- a/Lebesgue/LInt_p.v
+++ b/Lebesgue/LInt_p.v
@@ -606,7 +606,7 @@ eapply Rbar_le_trans.
 apply Inf_seq_minor with (n:=0%nat).
 apply Sup_seq_lub.
 intros n; apply LInt_p_monotone.
-intros x; rewrite plus_0_r.
+intros x; rewrite Nat.add_0_r.
 apply Hlimf.
 (* *)
 eapply Rbar_le_trans.
@@ -1371,7 +1371,7 @@ rewrite ex_lim_seq_Rbar_LimSup; try easy.
 unfold LimSup_seq_Rbar.
 apply Rbar_le_trans with (1:= Inf_seq_minor _ 0%nat).
 apply Sup_seq_lub.
-intros n; rewrite plus_0_r; easy.
+intros n; rewrite Nat.add_0_r; easy.
 rewrite <- Hx; easy.
 apply LInt_p_ae_finite; try easy.
 simpl; auto with real.
diff --git a/Lebesgue/R_compl.v b/Lebesgue/R_compl.v
index f60e87eda59cdef64b340baac4864b82124608f6..66324b085bbf5526afd9c17275345d493b22fbce 100644
--- a/Lebesgue/R_compl.v
+++ b/Lebesgue/R_compl.v
@@ -18,7 +18,7 @@ COPYING file for more details.
 From Coq Require Import Lia Reals Lra.
 From Coquelicot Require Import Coquelicot.
 From Flocq Require Import Core. (* For Zfloor, Zceil. *)
-
+Require Import logic_compl.
 
 Section R_ring_compl.
 
@@ -246,9 +246,8 @@ generalize (Rinv_0_lt_compat (b - a) H1); intros H2.
 generalize (archimed_floor_ex (/ (b - a))); intros [n [_ Hn]].
 exists (Z.abs_nat n).
 rewrite INR_IZR_INZ, Zabs2Nat.id_abs, abs_IZR, Rabs_pos_eq.
-rewrite Rplus_comm, <- Rle_minus_r, <- (Rinv_involutive (b - a)).
+rewrite Rplus_comm, <- Rle_minus_r, <- (Rinv_inv (b - a)).
 apply Rinv_le_contravar; try easy; now apply Rlt_le.
-now apply not_eq_sym, Rlt_not_eq.
 apply IZR_le, Z.lt_succ_r, lt_IZR; unfold Z.succ; rewrite plus_IZR.
 now apply Rlt_trans with (/ (b - a)).
 (* *)
@@ -276,7 +275,7 @@ cut (j - i <= N)%nat; try auto with zarith.
 cut (i + (j - i) <= N)%nat; try auto with zarith.
 generalize (j-i)%nat.
 induction n; intros M1 M2.
-rewrite plus_0_r.
+rewrite Nat.add_0_r.
 apply Rle_refl.
 apply Rle_trans with (u (i + n)%nat).
 apply IHn; auto with zarith.
@@ -670,9 +669,8 @@ Lemma is_pos_mult_half_pow :
   forall (eps : posreal) n, 0 < pos eps * (/ 2) ^ S n.
 Proof.
 intros eps n.
-rewrite <- Rinv_pow.
+rewrite pow_inv.
 apply is_pos_div_2_pow.
-apply not_eq_sym, Rlt_not_eq, Rlt_0_2.
 Qed.
 
 Definition mk_pos_mult_half_pow : posreal -> nat -> posreal :=
@@ -1096,14 +1094,14 @@ rewrite H2; auto with real.
 generalize (LocallySorted_nth Rlt 0%R l); intros H4.
 apply Rlt_le_trans with (nth (S i) l 0).
 apply H4; auto with arith.
-case (le_lt_or_eq 0 (length l)); auto with zarith.
+case (Nat.lt_eq_cases 0 (length l)); auto with zarith.
 apply Rlt_increasing with (u:=fun n=> nth n l 0)
   (N:=(length l-1)%nat); try easy.
 intros; apply H4; easy.
 split; auto with zarith.
 intros l i j H1 H2 H3 H4.
-case (le_or_lt i j); intros H5.
-case (le_lt_or_eq i j H5); intros H6; try easy.
+case (Nat.le_gt_cases i j); intros H5.
+case (ifflr (Nat.lt_eq_cases i j) H5); intros H6; try easy.
 exfalso; apply H with l i j; auto.
 exfalso; apply H with l j i; auto.
 Qed.
@@ -1127,7 +1125,7 @@ intros Hn3.
 assert (T: In (nth 0 l2 0) l1).
 apply H.
 apply nth_In.
-case (le_lt_or_eq 0 (length l2)); auto with arith.
+case (ifflr (Nat.lt_eq_cases 0 (length l2))); auto with arith.
 intros V; absurd (l2 = nil); try easy.
 apply length_zero_iff_nil; auto.
 destruct (In_nth l1 _ 0 T) as (m,(Hm1,Hm2)).
@@ -1141,10 +1139,10 @@ rewrite <- Hnn.
 assert (T: In (nth n l2 0) l1).
 apply H.
 apply nth_In.
-apply le_trans with (1:=Hn2).
+apply Nat.le_trans with (1:=Hn2).
 auto with arith.
 destruct (In_nth l1 _ 0 T) as (m,(Hm1,Hm2)).
-case (le_or_lt n m); intros M.
+case (Nat.le_gt_cases n m); intros M.
 rewrite <- Hm2.
 apply Rlt_increasing with  (u:=fun i => nth i l1 0) (N:=(length l1-1)%nat); try assumption.
 intros j Hj; apply LocallySorted_nth; assumption.
@@ -1156,7 +1154,7 @@ apply Rle_lt_trans with (nth m l2 0).
 apply Hn1; auto with zarith.
 apply Rlt_le_trans with (nth (S m) l2 0).
 apply LocallySorted_nth; try assumption.
-apply lt_le_trans with (1:=M).
+apply Nat.lt_le_trans with (1:=M).
 generalize (Nat.le_min_r (length l1) (length l2)); lia.
 apply Rlt_increasing with (u:=fun i => nth i l2 0) (N:=(length l2-1)%nat); try assumption.
 intros j Hj; apply LocallySorted_nth; assumption.
@@ -1178,7 +1176,7 @@ apply Rle_antisym.
 apply Sorted_In_eq_eq_aux1; assumption.
 apply Sorted_In_eq_eq_aux1; try assumption.
 intros x; split; apply H.
-now rewrite Min.min_comm.
+now rewrite Nat.min_comm.
 Qed.
 
 Lemma Sorted_In_eq_eq_aux3:
@@ -1194,7 +1192,7 @@ assert (H: forall (l1 l2 : list R),
      l1 <> nil -> l2 <> nil ->
        (length l1 <= length l2)%nat).
 intros l1 l2 H V1 V2 Z1 Z2.
-case (le_or_lt (length l1) (length l2)); try easy; intros H3.
+case (Nat.le_gt_cases (length l1) (length l2)); try easy; intros H3.
 exfalso.
 assert (T: In (nth (length l2) l1 0) l1).
 apply nth_In; try easy.
@@ -1212,9 +1210,9 @@ lia.
 assert (length l2 <> 0)%nat; try lia.
 rewrite <- Hm2.
 apply Sorted_In_eq_eq_aux2; auto; try (split;easy).
-rewrite Min.min_r; lia.
+rewrite Nat.min_r; lia.
 intros l1 l2 H0 V1 V2 Z1 Z2.
-apply le_antisym.
+apply Nat.le_antisymm.
 apply H; assumption.
 apply H; try assumption.
 intros x; split; apply H0; easy.
@@ -1232,7 +1230,7 @@ generalize (Sorted_In_eq_eq_aux3 l1 l2 H V1 V2 Z1 Z2).
 generalize (Sorted_In_eq_eq_aux2 l1 l2 H V1 V2 Z1 Z2).
 intros H3 H4.
 rewrite H4 in H3.
-rewrite Min.min_r in H3; try lia.
+rewrite Nat.min_r in H3; try lia.
 generalize H3 H4; clear V1 V2 H H3 H4 Z1 Z2; generalize l1 l2; clear l1 l2.
 induction l1.
 intros l2 H1 H2.
diff --git a/Lebesgue/Rbar_compl.v b/Lebesgue/Rbar_compl.v
index baa5c04253aef75464e3c99e7784a23478e06de7..e1d920ed2ac55cd98c6868213ee90fa5e8614c35 100644
--- a/Lebesgue/Rbar_compl.v
+++ b/Lebesgue/Rbar_compl.v
@@ -595,7 +595,7 @@ cut (j-i <= N)%nat; try auto with zarith.
 cut (i+ (j-i) <= N)%nat; try auto with zarith.
 generalize ((j-i))%nat.
 induction n; intros M1 M2.
-rewrite plus_0_r.
+rewrite Nat.add_0_r.
 apply Rbar_le_refl.
 trans (u (i+n)%nat).
 apply IHn; auto with zarith.
@@ -615,7 +615,7 @@ cut (j-i <= N)%nat; try auto with zarith.
 cut (i+ (j-i) <= N)%nat; try auto with zarith.
 generalize ((j-i))%nat.
 induction n; intros M1 M2.
-rewrite plus_0_r.
+rewrite Nat.add_0_r.
 apply Rbar_le_refl.
 trans (u (i+n)%nat).
 apply IHn; auto with zarith.
@@ -2510,7 +2510,7 @@ assert (J2: forall n, (N <= n)%nat -> f n = f N).
 induction n.
 auto with arith.
 intros H3.
-case (le_or_lt N n); intros H4.
+case (Nat.le_gt_cases N n); intros H4.
 rewrite <- H2; auto.
 replace (S n) with N; auto with arith.
 assert (J3: forall m n, (m <= n)%nat -> Rbar_le (f m) (f n)).
@@ -2521,7 +2521,7 @@ intros _; trans (f n).
 apply IHn; auto with arith.
 induction n.
 intros H3; contradict H3; auto with arith.
-intros H4; case (le_or_lt (S m) n); intros H5.
+intros H4; case (Nat.le_gt_cases (S m) n); intros H5.
 trans (f n).
 apply IHn; auto with arith.
 replace (S n) with (S m).
@@ -2529,7 +2529,7 @@ apply Rbar_le_refl.
 auto with arith.
 assert (J1: forall n, Rbar_le (f n) (f N)).
 intros n.
-case (le_or_lt n N); intros H3.
+case (Nat.le_gt_cases n N); intros H3.
 apply J3; auto.
 rewrite J2; auto with arith.
 (* *)
@@ -3344,14 +3344,14 @@ rewrite H2; rewrite <- Rbar_plus_minus_r; try easy.
 apply Rbar_lt_le; apply Rbar_le_lt_trans with (l - pos_div_2 eps).
 apply Rbar_eq_le; rewrite <- H2; simpl; f_equal; ring.
 apply Hn2.
-apply le_trans with (Init.Nat.max n1 n2)%nat.
+apply Nat.le_trans with (Init.Nat.max n1 n2)%nat.
 apply Nat.le_max_r.
 auto with arith.
 apply Rbar_plus_le_reg_r with l; try easy.
 rewrite H2; rewrite <- Rbar_plus_minus_r; try easy.
 apply Rbar_lt_le; apply Rbar_lt_le_trans with (l + pos_div_2 eps).
 apply Hn1.
-apply le_trans with (Init.Nat.max n1 n2)%nat.
+apply Nat.le_trans with (Init.Nat.max n1 n2)%nat.
 apply Nat.le_max_l.
 auto with arith.
 apply Rbar_eq_le; rewrite <- H2; simpl; f_equal; ring.
diff --git a/Lebesgue/Subset_finite.v b/Lebesgue/Subset_finite.v
index 676b52d45b9da8cf6c51d4d4b199a46328f55d84..d5a5065e8e928144582a79263e5b3059741f516c 100644
--- a/Lebesgue/Subset_finite.v
+++ b/Lebesgue/Subset_finite.v
@@ -88,14 +88,14 @@ Lemma shift_add :
     shift (shift A N1) N2 = shift A (N1 + N2).
 Proof.
 intros; apply functional_extensionality.
-intros n; unfold shift; now rewrite plus_assoc.
+intros n; unfold shift; now rewrite Nat.add_assoc.
 Qed.
 
 Lemma shift_assoc :
   forall (A : nat -> U -> Prop) N1 N2 n,
     shift A N1 (N2 + n) = shift A (N1 + N2) n.
 Proof.
-intros; unfold shift; now rewrite plus_assoc.
+intros; unfold shift; now rewrite Nat.add_assoc.
 Qed.
 
 End Def0_Facts.
@@ -481,7 +481,7 @@ Proof.
 split; intros H.
 (* *)
 intros n1 n2 Hn1 Hn2 Hn x Hx1 Hx2; contradict Hn.
-apply le_not_lt; rewrite Nat.le_lteq; right; symmetry.
+apply Nat.le_ngt; rewrite Nat.le_lteq; right; symmetry.
 now apply (H n1 n2 x).
 (* *)
 intros n1 n2 x Hn1 Hn2 Hx1 Hx2.
@@ -799,7 +799,7 @@ intros x [[n [Hn Hx]] | [n [Hn Hx]]].
 exists n; split; try lia.
 unfold append; now case (lt_dec n (S N)).
 exists (S N + n); split; try lia.
-unfold append; case (lt_dec (S N + n) (S N)); try lia; intros Hn'; now rewrite minus_plus.
+unfold append; case (lt_dec (S N + n) (S N)); try lia; intros Hn'; now rewrite Nat.add_comm, Nat.add_sub.
 (* *)
 intros x [n [Hn Hx]]; generalize Hx; clear Hx;
     unfold append; case (lt_dec n (S N)); intros Hn' Hx.
@@ -1081,7 +1081,7 @@ assert (Hf : forall n, n < S N -> f n < S M /\ A n (f n) x).
   apply (Hf' (exist _ n Hn')).
 exists (psi f); split.
 (* . *)
-unfold P; rewrite <- S_pred_pos; try (apply S_pow_pos; lia).
+unfold P; rewrite Nat.succ_pred_pos; try (apply S_pow_pos; lia).
 apply H2; intros n; now apply Hf.
 (* . *)
 intros n Hn; rewrite H4; try easy.
@@ -1089,7 +1089,7 @@ now apply Hf.
 intros n' Hn'; now apply Hf.
 (* *)
 intros [p [Hp Hx]] n Hn.
-unfold P in Hp; rewrite <- S_pred_pos in Hp; try (apply S_pow_pos; lia).
+unfold P in Hp; rewrite Nat.succ_pred_pos in Hp; try (apply S_pow_pos; lia).
 exists (phi p n); split; [apply H1 | apply Hx]; assumption.
 Qed.
 
diff --git a/Lebesgue/Subset_seq.v b/Lebesgue/Subset_seq.v
index 1480f09f63e7d40a704d781d36dbdc71bb44da33..2af84a50ad2c61c9a73633903f411fc98244efec 100644
--- a/Lebesgue/Subset_seq.v
+++ b/Lebesgue/Subset_seq.v
@@ -37,7 +37,7 @@ Context {U : Type}. (* Universe. *)
 Variable A B : nat -> U -> Prop. (* Subset sequences. *)
 
 Definition mix : nat -> U -> Prop :=
-  fun n => if even_odd_dec n then A (Nat.div2 n) else B (Nat.div2 n).
+  fun n => if Nat.Even_Odd_dec n then A (Nat.div2 n) else B (Nat.div2 n).
 
 End Def0.
 
@@ -1187,7 +1187,7 @@ Lemma liminf_shift :
 Proof.
 intros A N1; apply subset_ext; split; intros [N2 Hx].
 rewrite shift_add in Hx; now exists (N1 + N2).
-exists N2; intros n; rewrite shift_add, plus_comm.
+exists N2; intros n; rewrite shift_add, Nat.add_comm.
 specialize (Hx (N1 + n)); now rewrite shift_assoc in Hx.
 Qed.
 
@@ -1197,7 +1197,7 @@ Lemma limsup_shift :
 Proof.
 intros A N1; apply subset_ext; subset_lim_unfold; split; intros Hx N2.
 specialize (Hx N2); destruct Hx as [n Hx];
-    exists (N1 + n); now rewrite shift_assoc, plus_comm, <- shift_add.
+    exists (N1 + n); now rewrite shift_assoc, Nat.add_comm, <- shift_add.
 specialize (Hx (N1 + N2)); now rewrite shift_add.
 Qed.
 
@@ -1206,7 +1206,7 @@ Lemma incl_liminf_limsup :
     incl (liminf A) (limsup A).
 Proof.
 intros A x [n H] p; exists n.
-unfold shift; rewrite plus_comm; apply H.
+unfold shift; rewrite Nat.add_comm; apply H.
 Qed.
 
 Lemma compl_liminf :
diff --git a/Lebesgue/Tonelli.v b/Lebesgue/Tonelli.v
index dbf24eefbf324489cdb9af027d2c6e4189b14d9f..2fe11035103a0633cd873289584eb1002ba52333 100644
--- a/Lebesgue/Tonelli.v
+++ b/Lebesgue/Tonelli.v
@@ -291,7 +291,7 @@ intros (n,(Hn1,Hn2)); exists n; split; auto with arith.
 apply measurable_fun_ext with
    (f1:= fun x1 : X1 => sum_Rbar N (fun m : nat => muX2 (fun x2 : X2 => B m (x1, x2)))).
 intros x1; symmetry; apply measure_additivity_finite.
-intros n H5; apply le_lt_n_Sm in H5.
+intros n H5; apply Nat.lt_succ_r in H5.
 apply (section_measurable _ _ (H2a n H5)).
 rewrite <- Subset_finite.disj_finite_equiv in H4.
 intros n m x2 Hn Hm HBn HBm.
diff --git a/Lebesgue/UniformSpace_compl.v b/Lebesgue/UniformSpace_compl.v
index 889d4da02dbef3178cf227d793c8f4249fbf9f35..2b510cd3545f4d93f64998bf1ed738d2545c3d41 100644
--- a/Lebesgue/UniformSpace_compl.v
+++ b/Lebesgue/UniformSpace_compl.v
@@ -437,8 +437,7 @@ rewrite plus_opp_l, plus_zero_l.
 replace (abs (/ (INR n + 1))) with (Rabs (/ (INR n + 1))); try easy.
 rewrite Rabs_pos_eq.
 2: apply Rlt_le, InvINRp1_pos.
-rewrite <- Rinv_involutive.
-2: apply Rgt_not_eq, Rlt_gt, cond_pos.
+rewrite <- Rinv_inv.
 apply Rinv_lt_contravar.
 2: apply Rlt_le_trans with (INR N + 1);
     [assumption | now apply Rplus_le_compat_r, le_INR].
diff --git a/Lebesgue/bochner_integral/BInt_Bif.v b/Lebesgue/bochner_integral/BInt_Bif.v
index f5f10bcf70dc7514503d039ba5e026be85e738e8..573ee79ffbdc0d59568a633d8e0fb566f1659a53 100644
--- a/Lebesgue/bochner_integral/BInt_Bif.v
+++ b/Lebesgue/bochner_integral/BInt_Bif.v
@@ -224,9 +224,9 @@ Section BInt_prop.
         rewrite Raxioms.Rplus_0_l in HsN.
         apply (Rbar_plus_lt_compat (LInt_p μ (λ x : X, (‖ f - s n ‖)%fn x)) (ɛ*/2)
                                     (LInt_p μ (λ x : X, (‖ f - s' n ‖)%fn x)) (ɛ*/2)).
-            apply HsN; apply Max.max_lub_l with N' => //.
+            apply HsN; apply Nat.max_lub_l with N' => //.
             rewrite (LInt_p_ext _ _ (λ x : X, (‖ f' - s' n ‖)%fn x)).
-            apply Hs'N'; apply Max.max_lub_r with N => //.
+            apply Hs'N'; apply Nat.max_lub_r with N => //.
             move => x; unfold fun_norm, fun_plus.
             rewrite Ext => //.
             simpl; rewrite Rlimit.eps2 => //.
diff --git a/Lebesgue/bochner_integral/BInt_sf.v b/Lebesgue/bochner_integral/BInt_sf.v
index 3cf2f5bca6bf5baee470e440c849a5d1cfb4314a..cdbe10ff2dca29ac7c9fa48aa0ea0d002630b555 100644
--- a/Lebesgue/bochner_integral/BInt_sf.v
+++ b/Lebesgue/bochner_integral/BInt_sf.v
@@ -34,6 +34,7 @@ Require Import
     sigma_algebra
     sum_Rbar_nonneg
     Rbar_compl
+    logic_compl
 .
 
 Require Import
@@ -488,9 +489,8 @@ Section BInt_sf_plus.
         congr plus; apply sum_n_ext_loc.
             replace (val sf_f) with vf by rewrite Eqf => //.
             move => k1 Hk1.
-            case (le_lt_or_eq k1 maxf) => //.
+            case (ifflr (Nat.lt_eq_cases k1 maxf)) => //.
                 move => Hk1'.
-                congr scal.
                 replace (which sf_f) with wf by rewrite Eqf => //.
                 rewrite sum_n_sum_Rbar.
                     all : swap 1 2.
@@ -522,9 +522,8 @@ Section BInt_sf_plus.
                 rewrite axf1; do 2 rewrite scal_zero_r => //.
             replace (val sf_g) with vg by rewrite Eqg => //.
             move => k2 Hk2.
-            case (le_lt_or_eq k2 maxg) => //.
+            case (ifflr (Nat.lt_eq_cases k2 maxg)) => //.
                 move => Hk2'.
-                congr scal.
                 replace (which sf_g) with wg by rewrite Eqg => //.
                 rewrite sum_n_sum_Rbar.
                     all : swap 1 2.
@@ -707,7 +706,7 @@ Section BInt_sf_norm.
             all : swap 1 2.
             rewrite Eqf => /=.
             unfold abs => /= n Hn.
-            case: (le_lt_or_eq n maxf) => // Hn'; clear Hn.
+            case: (ifflr (Nat.lt_eq_cases n maxf)) => // Hn'; clear Hn.
             rewrite Rabs_pos_eq => //.
             unfold nth_carrier => /=.
             pose Le0μn := meas_nonneg _ μ (λ x : X, vf x = n); clearbody Le0μn.
@@ -758,7 +757,7 @@ Section BInt_well_defined.
         replace (which sf) with wf by rewrite Eqf => //.
         replace (max_which sf) with maxf in Hn
             by rewrite Eqf => //.
-        case: (le_lt_or_eq n maxf) => // Hn'.
+        case: (ifflr (Nat.lt_eq_cases n maxf)) => // Hn'.
             (* pose Hμn := axf4 n Hn'; clearbody Hμn; unfold is_finite in Hμn. *)
             pose Le0μn := meas_nonneg _ μ (λ x : X, wf x = n); clearbody Le0μn.
             case: (Rbar_le_cases _ Le0μn).
diff --git a/Lebesgue/bochner_integral/Bi_fun.v b/Lebesgue/bochner_integral/Bi_fun.v
index 6461477e59e492efc0a2941a53d415d99d2b751e..330e0959aec9b3d8be3ebad764ce3831a58feeed 100644
--- a/Lebesgue/bochner_integral/Bi_fun.v
+++ b/Lebesgue/bochner_integral/Bi_fun.v
@@ -52,6 +52,7 @@ Require Import
     sigma_algebra_R_Rbar
     sum_Rbar_nonneg
     R_compl
+    logic_compl
 .
 
 
@@ -95,14 +96,14 @@ Proof.
         pose sigÉ›' := RIneq.mkposreal (/a * É›) H.
         case: (Hl sigÉ›') => HÉ›'1 HÉ›'2.
         case: HÉ›'2 => N' HN'.
-        assert (N' ≤ max N N') by apply Max.le_max_r.
+        assert (N' ≤ max N N') by apply Nat.le_max_r.
         case: (HÉ›'1 (max N N')) => N'' [HN'' HN''lt].
         assert (N' ≤ N'').
             apply Nat.le_trans with (max N N') => //.
         pose Ineq := (HN' N'' H1); clearbody Ineq; simpl in Ineq.
         clear HN' H0; simpl in HN''lt.
-        exists N''; split; [apply Max.max_lub_l with N' => // | ].
-        assert (N' ≤ N'') by apply Max.max_lub_r with N => //.
+        exists N''; split; [apply Nat.max_lub_l with N' => // | ].
+        assert (N' ≤ N'') by apply Nat.max_lub_r with N => //.
         case_eq (u N'').
         all : swap 1 2.
         move => Abs.
@@ -565,8 +566,8 @@ Section Bif_op.
         rewrite Raxioms.Rplus_0_l in HgN'.
         apply (Rbar_plus_lt_compat (LInt_p μ (λ x : X, (‖ f - sf n ‖)%fn x)) (ɛ*/2)
                                     (LInt_p μ (λ x : X, (‖ g - sg n ‖)%fn x)) (ɛ*/2)).
-            apply HfN; apply Max.max_lub_l with N' => //.
-            apply HgN'; apply Max.max_lub_r with N => //.
+            apply HfN; apply Nat.max_lub_l with N' => //.
+            apply HgN'; apply Nat.max_lub_r with N => //.
             simpl; rewrite Rlimit.eps2 => //.
         all : swap 1 3.
         (**)
@@ -1142,7 +1143,7 @@ Module Bif_adapted_seq.
                 unfold whichn.
                 assert (biggestA n (f x) < n) as LtbigA.
                 pose LebigAnx := LebigAn (f x); clearbody LebigAnx; clear LebigAn.
-                case: (le_lt_or_eq _ _ LebigAnx) => //.
+                case: (ifflr (Nat.lt_eq_cases _ _) LebigAnx) => //.
                 move /biggestA_eq_max_spec => Abs.
                 pose Absm := Abs m Ltmn; clearbody Absm => //.
                 assert (biggestA n (f x) ≠ n) as NeqbigA by lia.
@@ -1221,7 +1222,7 @@ Module Bif_adapted_seq.
                         apply HA with j => //.
 
                 move => NHA.
-                case: (le_lt_or_eq _ _ (whichn_le_n n x)) => //.
+                case: (ifflr (Nat.lt_eq_cases _ _) (whichn_le_n n x)) => //.
                 move => Abs; apply False_ind.
                 assert (whichn n x = whichn n x) as TrivEq by easy.
                 move: TrivEq => / (whichn_spec_lt_n n (whichn n x) Abs x); case => j [Ltjn [[Ajx _] _]].
@@ -1254,7 +1255,7 @@ Module Bif_adapted_seq.
                 → measurable gen (λ x : X, whichn n x = j).
         Proof.
             move => j Lejn.
-            case: (le_lt_or_eq _ _ Lejn).
+            case: (ifflr (Nat.lt_eq_cases _ _) Lejn).
                 move => Ltjn.
                 apply measurable_ext with (fun x =>
                     ∃ m : nat, m < n ∧
@@ -1315,7 +1316,7 @@ Module Bif_adapted_seq.
         Proof.
             move => x.
             unfold sp => /=.
-            case: (le_lt_or_eq _ _ (whichn_le_n n x)); swap 1 2.
+            case: (ifflr (Nat.lt_eq_cases _ _) (whichn_le_n n x)); swap 1 2.
                     move => Eqn; rewrite Eqn ax_val_max_which_n norm_zero.
                     replace 0 with (2 * 0).
                         2 : apply RIneq.Rmult_0_r.
@@ -1390,7 +1391,7 @@ Module Bif_adapted_seq.
                     assumption.
                     assumption.
             assert (whichn n x < n)%nat as Ltwnxn.
-                case: (le_lt_or_eq _ _ (whichn_le_n n x)) => //.
+                case: (ifflr (Nat.lt_eq_cases _ _) (whichn_le_n n x)) => //.
                 move => /whichn_spec_eq_n Abs.
                 apply False_ind, Abs.
                 exists m.
diff --git a/Lebesgue/bochner_integral/Bsf_Lsf.v b/Lebesgue/bochner_integral/Bsf_Lsf.v
index 9c656c210beed24e380c30732f663a30bf14716b..1b741f261e099d83558461e86007711b4e09263c 100644
--- a/Lebesgue/bochner_integral/Bsf_Lsf.v
+++ b/Lebesgue/bochner_integral/Bsf_Lsf.v
@@ -38,6 +38,7 @@ Require Import
     sigma_algebra
     measure
     simple_fun
+    logic_compl
 .
 
 Require Import
@@ -364,7 +365,7 @@ Section Bochner_sf_Lebesgue_sf.
                                 unfold nth_carrier, fun_sf => ->.
                                 rewrite Eqf => /=; auto.
                                 case; unfold nth_carrier, fun_sf => Eq_sfx_vfn Le_wfx_n.
-                                case (le_lt_or_eq (which sf x) n) => //.
+                                case (ifflr (Nat.lt_eq_cases (which sf x) n)) => //.
                                 apply le_S_n => //.
                                 move /Pl; unfold fun_sf; rewrite Eq_sfx_vfn.
                                 move /NIn_vfn => //.
@@ -427,7 +428,7 @@ Section Bochner_sf_Lebesgue_sf.
                 congr Rbar_mult.
                 apply measure_ext => x; split; swap 1 2.
                     case => H1 H2; split; [assumption | lia].
-                    move => [Eq_sfx_y /le_S_n/le_lt_or_eq].
+                    move => [Eq_sfx_y /le_S_n/Nat.lt_eq_cases].
                     case => //.
                     move => Eq_wsfx_n; apply False_ind.
                     unfold fun_sf in Eq_sfx_y.
@@ -437,7 +438,7 @@ Section Bochner_sf_Lebesgue_sf.
 
                 move => In_vfn.
                 apply: (exist _ l); split.
-                move => x /le_S_n/le_lt_or_eq; case.
+                move => x /le_S_n/Nat.lt_eq_cases; case.
                     apply Pl.
                     unfold fun_sf => ->; rewrite Eqf => //.
 
@@ -456,7 +457,7 @@ Section Bochner_sf_Lebesgue_sf.
                         2 : apply ax_measurable; rewrite Eqf => //.
                         2 : lia.
                     apply measure_ext => x; split.
-                        move => [Eq_sfx_y /le_S_n/le_lt_or_eq].
+                        move => [Eq_sfx_y /le_S_n/Nat.lt_eq_cases].
                         case.
                             move => Hlt; left; easy.
                             move => Heq; right.
@@ -538,7 +539,7 @@ Section Bochner_sf_Lebesgue_sf.
                             move => [Abs _]; rewrite Abs in Hb => //.
                             apply False_ind.
                         2, 3 : assumption.
-                    case: (le_lt_or_eq n maxf Lenmaxf).
+                    case: (ifflr (Nat.lt_eq_cases n maxf) Lenmaxf).
                         move => Ltnmaxf.
                         rewrite Rbar_mult_comm Rbar_mult_finite_real.
                             all : swap 1 2.
diff --git a/Lebesgue/bochner_integral/simpl_fun.v b/Lebesgue/bochner_integral/simpl_fun.v
index 9ec1fe926680888061f7508b2b2ca5a9a1f504e4..d3e5d6fd944c54b8bf6550653d775ca7ec333900 100644
--- a/Lebesgue/bochner_integral/simpl_fun.v
+++ b/Lebesgue/bochner_integral/simpl_fun.v
@@ -40,6 +40,7 @@ Require Import
     measurable_fun
     LInt_p
     R_compl
+    logic_compl
 .
 
 Require Import
@@ -548,7 +549,7 @@ Section simpl_fun_plus.
         assert
             (n <= max_which)
             as Le_n_mw.
-            apply le_Sn_le => //.
+            apply Nat.lt_le_incl => //.
         pose Hnfng := confined_square_inv maxg maxf n Le_n_mw; clearbody Hnfng.
         fold c in Hnfng; rewrite Eqc in Hnfng; case: Hnfng => Hnf Hng.
         assert
@@ -882,7 +883,7 @@ Section simpl_fun_meas.
         move => y Hy.
         rewrite sf_decomp_preim_which.
         apply finite_sum_Rbar => k Hk.
-        case: (le_lt_or_eq k (max_which sf) Hk) => Hkmaxf.
+        case: (ifflr (Nat.lt_eq_cases k (max_which sf)) Hk) => Hkmaxf.
             apply Rbar_bounded_is_finite with (real 0%R) (μ (λ x : X, which sf x = k)).
             apply meas_nonneg.
             apply (measure_le _ μ (λ x : X, val sf k = y ∧ which sf x = k) (fun x => which sf x = k)).
@@ -967,7 +968,7 @@ Section simpl_fun_meas.
         apply ax_measurable; lia.
         move => x Neq0.
         exists (which sf x); split => //.
-        case: (le_lt_or_eq _ _ (ax_which_max_which sf x)) => //.
+        case: (ifflr (Nat.lt_eq_cases _ _) (ax_which_max_which sf x)) => //.
         move => Abs.
         unfold fun_sf in Neq0.
         rewrite Abs in Neq0.
@@ -975,7 +976,7 @@ Section simpl_fun_meas.
         easy.
         rewrite (measure_decomp_finite _ μ _ (max_which sf) (fun n => fun x => which sf x = n)).
         apply finite_sum_Rbar => k Hk.
-        case: (le_lt_or_eq _ _ Hk) => Hk'.
+        case: (ifflr (Nat.lt_eq_cases _ _) Hk) => Hk'.
         rewrite (measure_ext _ _ _ (λ x : X, which sf x = k)).
         rewrite Eqf in Hk' |- * => /=; simpl in Hk'.
         apply axf4 => //.
@@ -1043,7 +1044,7 @@ Section simpl_fun_nonzero.
             exists sf'n; repeat split => //.
             lia.
             move => k.
-            move => /le_lt_or_eq; case.
+            move => /Nat.lt_eq_cases; case.
             move => H1 H2.
             apply IHn.
             1, 2 : lia.
@@ -1103,7 +1104,7 @@ Section simpl_fun_nonzero.
                 k ≤ maxSn
                 → measurable gen (λ x : X, whichSn x = k)) as axSn3.
             move => k Hk; unfold whichSn.
-            case: (le_lt_or_eq _ _ Hk); swap 1 2.
+            case: (ifflr (Nat.lt_eq_cases _ _) Hk); swap 1 2.
             move => ->.
             apply measurable_ext with (fun (x : X) => whichn x = m ∨ whichn x = maxn).
             move => x; split.
@@ -1233,7 +1234,7 @@ Section simpl_fun_nonzero.
             | S l => n - l
             end) with ((S n) - (max_which sf - maxSn)) in Hk1.
             2 : case: (max_which sf - maxSn) => //.
-            case: (le_lt_or_eq _ _ Hk1).
+            case: (ifflr (Nat.lt_eq_cases _ _) Hk1).
             move => Hkn.
             case: IHn => IHn1 IHn2.
             rewrite Eqsfn in IHn2; simpl in IHn2.
diff --git a/Lebesgue/bochner_integral/square_bij.v b/Lebesgue/bochner_integral/square_bij.v
index f4f892a7e28fad43c51dd7396dfdb6beda349209..82c9d18e141f4f5a8cb6915fb2a0e3a1ee9314ab 100644
--- a/Lebesgue/bochner_integral/square_bij.v
+++ b/Lebesgue/bochner_integral/square_bij.v
@@ -119,8 +119,8 @@ Section square_bij_prop.
             with
             ((n' * S n) + n)
             by lia.
-        apply plus_le_compat => //.
-        apply mult_le_compat => //.
+        apply Nat.add_le_mono => //.
+        apply Nat.mul_le_mono => //.
     Qed.
 
 End square_bij_prop.
diff --git a/Lebesgue/countable_sets.v b/Lebesgue/countable_sets.v
index 64c81bdd5f932a2f2e337e61b8b673e730c4bd62..be0282b83a3a78aad0e3e95505349153b1fc0d2d 100644
--- a/Lebesgue/countable_sets.v
+++ b/Lebesgue/countable_sets.v
@@ -22,16 +22,13 @@ Require Import logic_compl. (* For strong_induction. *)
 Lemma Nat_div2_gt : forall a b, (2 * a + 1 < b)%nat -> (a < Nat.div2 b)%nat.
 Proof.
 intros a b H.
-assert (2*a < 2*Nat.div2 b)%nat.
-2: auto with zarith.
-apply plus_lt_reg_l with 1%nat.
-rewrite Arith.Plus.plus_comm.
-apply lt_le_trans with (1:=H).
-replace (2*Nat.div2 b)%nat with (Nat.double (Nat.div2 b)).
-2: unfold Nat.double; ring.
-case (even_odd_dec b); intros Hb.
-rewrite <- Div2.even_double; auto with arith.
-rewrite Div2.odd_double at 1; auto with arith.
+apply Nat.mul_lt_mono_pos_l with (p:=2%nat); try (constructor; easy).
+destruct (Nat.Even_Odd_dec b) as [[b' ->]%Nat.Even_EvenT | [b' ->]%Nat.Odd_OddT].
+- rewrite Nat.div2_double; try easy.
+  apply (Nat.lt_trans _ (2 * a + 1) _); try easy.
+  now rewrite Nat.add_1_r; constructor.
+- rewrite Nat.add_1_r, Nat.div2_succ_double.
+  now rewrite (Nat.add_lt_mono_r _ _ 1).
 Qed.
 
 Lemma Zabs_nat_Zopp : forall z, Z.abs_nat (-z) = Z.abs_nat z.
@@ -49,7 +46,7 @@ Definition bij_ZN : Z -> nat :=
     end.
 
 Definition bij_NZ : nat -> Z :=
-  fun n => match even_odd_dec n with
+  fun n => match Nat.Even_Odd_dec n with
     | left _ => (Z.of_nat (Nat.div2 n))%Z
     | right _ => (- Z.of_nat (Nat.div2 (n + 1)))%Z
     end.
@@ -69,42 +66,39 @@ auto with zarith.
 auto with zarith.
 intros; auto with arith.
 unfold bij_NZ.
-case (even_odd_dec _); intros H2.
+case (Nat.Even_Odd_dec _); intros H2.
 contradict H2; intros H2.
-apply (not_even_and_odd (2*Z.abs_nat z-1)); try easy.
+
+apply (Nat.Even_Odd_False (2*Z.abs_nat z-1)); try easy.
 case_eq (Z.abs_nat z).
 intros K; contradict H; auto with zarith.
 intros n Hn.
 replace (2*S n -1)%nat with (2*n +1)%nat by auto with zarith.
-apply odd_plus_r.
-apply even_mult_l.
-apply even_S, odd_S, even_O.
-apply odd_S, even_O.
+now apply Nat.OddT_Odd; exists n.
 replace ((2 * Z.abs_nat z - 1 + 1))%nat with (2*(Z.abs_nat z))%nat.
 rewrite div2_double.
 rewrite Nat2Z.inj_abs_nat.
 rewrite Z.abs_neq; auto with zarith.
 auto with zarith.
 unfold bij_NZ.
-case (even_odd_dec _); intros H2.
+case (Nat.Even_Odd_dec _); intros H2.
 rewrite div2_double.
 rewrite Nat2Z.inj_abs_nat.
 rewrite Z.abs_eq; auto with zarith.
 contradict H2; intros H2.
-apply (not_even_and_odd (2*Z.abs_nat z)); try easy.
-apply even_mult_l.
-apply even_S, odd_S, even_O.
+apply (Nat.Even_Odd_False(2*Z.abs_nat z)); try easy.
+now apply Nat.EvenT_Even; exists (Z.abs_nat z).
 Qed.
 
 Lemma bij_ZNZ : forall n, bij_ZN (bij_NZ n) = n.
 Proof.
 intros n; unfold bij_NZ.
-case (even_odd_dec n); intros H1.
+case (Nat.Even_Odd_dec n); intros H1.
 unfold bij_ZN.
 case (Z_lt_le_dec _ 0); intros H2.
 contradict H2; auto with zarith.
 rewrite Zabs2Nat.id.
-rewrite Div2.even_double; try assumption.
+rewrite Nat.Even_double; try assumption.
 unfold Nat.double; auto with zarith.
 unfold bij_ZN.
 case (Z_lt_le_dec _ 0); intros H2.
@@ -118,18 +112,18 @@ simpl (Z.of_nat 2); simpl (Z.of_nat 1); rewrite Z.opp_involutive.
 apply trans_eq with (-1+(Z.of_nat (Nat.div2 (n + 1))+Z.of_nat (Nat.div2 (n + 1))))%Z.
 ring.
 rewrite <- Nat2Z.inj_add.
-generalize (Div2.even_double (n+1)); unfold Nat.double.
+generalize (Nat.Even_double (n+1)); unfold Nat.double.
 intros T; rewrite <- T.
 rewrite Nat2Z.inj_add; simpl (Z.of_nat 1); ring.
 replace (n+1)%nat with (S n) by auto with zarith.
-now apply even_S.
+now apply Nat.Even_alt_Even; apply Nat.Odd_alt_Odd in H1; constructor.
 assert (1 <= Z.abs_nat (- Z.of_nat (Nat.div2 (n + 1))))%nat.
 2: auto with zarith.
 rewrite Zabs_nat_Zopp.
 replace 1%nat with (Z.abs_nat 1) at 1 by easy.
 apply Zabs_nat_le; split; auto with zarith.
 case_eq n.
-intros K; contradict H1; rewrite K; easy.
+now intros ->.
 intros m Hm.
 contradict H2; apply Zlt_not_le.
 assert (0 < Nat.div2 (n+1))%nat.
@@ -147,7 +141,7 @@ Section N2_countable.
 Fixpoint bij_NN2_aux (n p : nat) : nat * nat :=
   match p with
   | O => (0, 0)%nat
-  | S p' =>  match even_odd_dec n with
+  | S p' =>  match Nat.Even_Odd_dec n with
     | left _ =>
       let (u1, v1) := bij_NN2_aux (Nat.div2 n) p' in
       (S u1, v1)
@@ -195,15 +189,15 @@ apply sym_not_eq, Nat.lt_neq.
 apply Nat_div2_gt.
 assert (n <> 0)%nat; auto with zarith.
 intros K; contradict e; rewrite K; intros K'.
-apply (not_even_and_odd 1); try easy.
-apply odd_S, even_O.
+apply (Nat.Even_Odd_False 1); try easy.
+now exists 0%nat.
 apply H with p'; try assumption.
-apply Div2.lt_div2; auto with zarith.
+apply Nat.lt_div2; auto with zarith.
 assert (Nat.div2 (S n) < S n)%nat; auto with zarith.
-apply Div2.lt_div2; auto with zarith.
+apply Nat.lt_div2; auto with zarith.
 destruct (bij_NN2_aux (Nat.div2 (S n)) p').
 rewrite Hu, Hv; simpl; auto with zarith.
-rewrite (Div2.even_double _ e), H4.
+rewrite (Nat.Even_double _ e), H4.
 replace u with (S (pred u)) at 2.
 2: rewrite Hu; auto with zarith.
 rewrite Nat.pow_succ_r.
@@ -217,32 +211,30 @@ rewrite H3; easy.
 assert (Hv: (v = Nat.div2 (S n))%nat).
 apply trans_eq with (snd (u,v)); try easy.
 rewrite H3; easy.
-rewrite (Div2.odd_double _ o), Hu, Hv.
+rewrite (Nat.Odd_double _ o), Hu, Hv.
 unfold Nat.double; simpl (2^0)%nat.
 ring.
 Qed.
 
 Lemma bij_NN2_aux_u :
   forall u v u' v',
-    (Nat.pow 2 u * (S (2 * v)) = Nat.pow 2 u' * (S (2 * v')))%nat ->
+    (2 ^ u * (S (2 * v)) = 2 ^ u' * (S (2 * v')))%nat ->
     (u,v) = (u',v').
 Proof.
 assert (Hu: forall u v u' v', (u < u')%nat ->
-  (Nat.pow 2 u * (S (2*v)) = Nat.pow 2 u' * (S (2*v')))%nat ->
+  (2 ^ u * (S (2*v)) = 2 ^ u' * (S (2*v')))%nat ->
   False).
 intros u v u' v' H1 H2.
-apply (not_even_and_odd (2^(u'-u)*(S (2*v'))))%nat.
-apply even_mult_l.
+apply (Nat.Even_Odd_False (2^(u'-u)*(S (2*v'))))%nat.
+apply Nat.Even_mul_l.
 case_eq (u'-u)%nat.
 intros K; contradict K; auto with zarith.
 intros j Hj; rewrite Nat.pow_succ_r.
-apply even_mult_l.
-apply even_S, odd_S, even_O.
+apply Nat.Even_mul_l.
+now exists 1%nat.
 auto with arith.
 replace (2 ^ (u' - u) * S (2 * v'))%nat with (S (2*v)).
-apply odd_S.
-apply even_mult_l.
-apply even_S, odd_S, even_O.
+now exists v; rewrite Nat.add_1_r.
 apply Nat.mul_cancel_l with (Nat.pow 2 u).
 apply Nat.pow_nonzero; auto with arith.
 rewrite H2, Nat.mul_assoc.
@@ -251,8 +243,8 @@ f_equal; f_equal.
 auto with zarith.
 (* *)
 intros u v u' v' H.
-case (le_or_lt u u'); intros H1.
-case (le_lt_or_eq _ _ H1); intros H2.
+case (Nat.le_gt_cases u u'); intros H1.
+case (ifflr (Nat.lt_eq_cases _ _) H1); intros H2.
 absurd (False); try easy.
 apply (Hu u v u' v'); easy.
 rewrite H2.
@@ -285,7 +277,7 @@ intros u v H.
 apply bij_NN2_aux_u.
 rewrite <- bij_NN2_aux_p with (S (Init.Nat.pred (2 ^ n * S (m + (m + 0)))))
    (S (Init.Nat.pred (2 ^ n * S (m + (m + 0))))) u v; try easy.
-rewrite <- (S_pred _ 0%nat); try easy.
+rewrite Nat.succ_pred_pos; try easy.
 apply Nat.mul_pos_pos; auto with zarith.
 assert (Nat.pow 2 n <> 0)%nat; auto with zarith.
 apply Nat.pow_nonzero; auto with zarith.
diff --git a/Lebesgue/list_compl.v b/Lebesgue/list_compl.v
index 53bfd5ff3cf933027537eac4bde374da8374ecb5..97e1d32d0fcf9ad7dfcdeebcbc7583ba4aff6ba2 100644
--- a/Lebesgue/list_compl.v
+++ b/Lebesgue/list_compl.v
@@ -217,7 +217,7 @@ induction l; try easy.
 intros i Hi; simpl.
 apply in_inv in Hi; destruct Hi as [Hi | Hi].
 rewrite Hi; apply Nat.le_max_l.
-apply le_trans with (max_l l).
+apply Nat.le_trans with (max_l l).
 now apply IHl.
 apply Nat.le_max_r.
 Qed.
diff --git a/Lebesgue/logic_compl.v b/Lebesgue/logic_compl.v
index ed368b7129db81e7a99b9f87e7ad72075f023f8a..8869ca636a9eb0945fd4191b310aa96737da7b16 100644
--- a/Lebesgue/logic_compl.v
+++ b/Lebesgue/logic_compl.v
@@ -31,19 +31,28 @@ intros k Hk.
 replace k with 0%nat.
 apply H.
 intros m Hm; contradict Hm.
-apply lt_n_0.
+apply Nat.nlt_0_r.
 generalize Hk; case k; trivial.
 intros m Hm; contradict Hm.
-apply le_not_lt.
+apply Nat.le_ngt.
 now auto with arith.
 intros k Hk.
 apply H.
 intros m Hm.
 apply IHn.
-apply lt_le_trans with (1:=Hm).
-now apply gt_S_le.
+apply Nat.lt_le_trans with (1:=Hm).
+now apply Nat.succ_le_mono.
 apply H0.
 apply le_n.
 Qed.
 
+Lemma ifflr {P} {Q} (h : P <-> Q) : P -> Q.
+Proof.
+  now destruct h as [pimqp _].
+Qed.
+
+Lemma iffrl {P} {Q} : P <-> Q -> Q -> P.
+Proof.
+  now intros [_ QimpP].
+Qed.
 End LT.
diff --git a/Lebesgue/measure.v b/Lebesgue/measure.v
index 2329625acc9084046f9a7c313a76abb18410b0e1..0f6f174c4a264ad1cd210cdd28f2e0825bae4801 100644
--- a/Lebesgue/measure.v
+++ b/Lebesgue/measure.v
@@ -316,7 +316,7 @@ intros [n [Hn K]]; case (excluded_middle_informative (A (S N) x)); intros HSN.
 now left.
 right; exists n; split; try easy; case (Nat.eq_dec n (S N)); intros J.
 contradict HSN; now rewrite <- J.
-apply lt_n_Sm_le; now destruct Hn; [ | auto with arith ].
+apply Nat.lt_succ_r; now destruct Hn; [ | auto with arith ].
 Qed.
 
 Lemma measure_union :
@@ -457,7 +457,7 @@ apply Inf_seq_decr_shift with (u := fun n => mu (A n)); intros n;
     apply measure_le; try easy; apply HA.
 apply functional_extensionality; intros x;
     apply propositional_extensionality; split; intros H n; try easy.
-  case (le_or_lt n0 n); intros Hn.
+  case (Nat.le_gt_cases n0 n); intros Hn.
   replace n with (n0 + (n - n0))%nat; [easy|auto with arith].
   apply subset_decr_shift with (n0 - n)%nat; try easy.
   replace (n + (n0 - n))%nat with (n0 + 0)%nat; [easy|lia].
diff --git a/Lebesgue/measure_R.v b/Lebesgue/measure_R.v
index 9bf8d69828983aceff176a41d3e112dc509d3ae4..f8db89331239a3666284671c4a754606dae75aac 100644
--- a/Lebesgue/measure_R.v
+++ b/Lebesgue/measure_R.v
@@ -23,7 +23,7 @@ Require Import nat_compl R_compl Rbar_compl.
 Require Import countable_sets LF_subcover sum_Rbar_nonneg.
 Require Import Subset.
 Require Import sigma_algebra sigma_algebra_R_Rbar.
-Require Import measure.
+Require Import measure logic_compl.
 
 Require Import measure_R_compl.
 
@@ -363,8 +363,7 @@ replace (bn (i (S p')) - an (i 0%nat))
     with (bn (i (S p')) + (0 - an (i 0%nat))) by field.
 apply Rplus_le_compat_l, Rplus_le_compat_r.
 rewrite <- Rminus_le_0.
-apply Rlt_le, Hip.
-apply le_lt_n_Sm in Hp'; lia.
+now apply Rlt_le, Hip.
 now apply (HH q).
 (* . *)
 trans (sum_Rbar (max_n i q) (fun p => bn p - an p)).
@@ -649,11 +648,10 @@ exists n; split; try easy; lia.
 exists (S N); now split.
 (* . *)
 intros [n [Hn Hx]].
-case (le_lt_eq_dec n (S N)); try easy; clear Hn; intros Hn.
-apply lt_n_Sm_le in Hn.
-left; exists n; tauto.
-rewrite Hn in Hx.
-now right.
+case (le_lt_eq_dec n (S N)). try easy; clear Hn; intros Hn.
+apply Nat.lt_succ_r in Hn.
+now left; exists n; split; try easy; try apply Nat.succ_le_mono.
+now intros ->; right.
 Qed.
 
 (* Lem 634 p. 100 *)
@@ -691,13 +689,13 @@ pose (E := fun n => match n with 0 => E1 | n => E2 end).
 apply cal_L_ext with (fun x => forall n, (n <= 1)%nat -> E n x).
 2: { apply cal_L_intersection_finite; intros n Hn.
     case (le_lt_eq_dec n 1); try easy; clear Hn; intros Hn.
-    apply lt_n_Sm_le, Nat.le_0_r in Hn.
+    apply Nat.lt_succ_r, Nat.le_0_r in Hn.
     all: now rewrite Hn. }
 intros x; split.
 intros H; split; [apply (H 0%nat) | apply (H 1%nat)]; lia.
 intros [Hx1 Hx2] n Hn.
 case (le_lt_eq_dec n 1); try easy; clear Hn; intros Hn.
-apply lt_n_Sm_le, Nat.le_0_r in Hn.
+apply Nat.lt_succ_r, Nat.le_0_r in Hn.
 all: now rewrite Hn.
 Qed.
 
@@ -947,8 +945,7 @@ destruct (nfloor_ex (/ (b - x))) as [n [_ Hn]].
 now apply Rlt_le, Rinv_0_lt_compat.
 exists n.
 rewrite Rle_minus_r, Rplus_comm, <- Rle_minus_r; apply Rlt_le.
-rewrite <- Rinv_involutive.
-2: apply not_eq_sym, Rlt_dichotomy_converse; now left.
+rewrite <- Rinv_inv.
 apply Rinv_lt_contravar; try easy.
 apply Rmult_lt_0_compat.
 now apply Rinv_0_lt_compat.
diff --git a/Lebesgue/measure_R_compl.v b/Lebesgue/measure_R_compl.v
index 81acf1a8301324823e0c5c45d00d74356e7d7621..e404cd686f86ef3b496f90707353c4105003cdfd 100644
--- a/Lebesgue/measure_R_compl.v
+++ b/Lebesgue/measure_R_compl.v
@@ -24,7 +24,7 @@ From Coquelicot Require Import Coquelicot.
 
 Require Import Rbar_compl sum_Rbar_nonneg.
 Require Import sigma_algebra sigma_algebra_R_Rbar.
-Require Import measure.
+Require Import measure logic_compl.
 
 
 Section my_subset_compl.
@@ -138,10 +138,11 @@ Lemma DU_equiv :
 Proof.
 intros A n x; destruct n; try easy.
 split; intros [HSn Hn]; split; try easy.
-intros p Hp Hp'; apply lt_n_Sm_le in Hp; apply Hn;
-    exists p; split; try easy; now apply DU_incl.
-intros Hp; destruct Hp as [p Hp];
-    apply (Hn p); try easy; now apply le_lt_n_Sm.
+intros p Hp Hp'; apply (Nat.lt_succ_r) in Hp; apply Hn.
+    exists p; split; try easy.
+    now apply Nat.succ_le_mono, Nat.succ_le_mono.
+intros Hp; destruct Hp as [p [plen HA]]; apply (Hn p); try easy.
+now apply Nat.succ_le_mono in plen.
 Qed.
 
 End my_subset_compl.
diff --git a/Lebesgue/measure_Radon.v b/Lebesgue/measure_Radon.v
index 066c1f58f04d2ffe66a2ba47c42059fd8f5433a8..c7ae8d7728d3e17a20672ae234a2ccd85a8a7fed 100644
--- a/Lebesgue/measure_Radon.v
+++ b/Lebesgue/measure_Radon.v
@@ -274,7 +274,7 @@ apply Rlt_not_le.
 apply Rplus_lt_reg_r with (/ (INR n + 1)); ring_simplify.
 apply Rplus_lt_reg_l with (- z); ring_simplify.
 replace (-z + x) with (x - z); try ring.
-rewrite <- Rinv_involutive.
+rewrite <- Rinv_inv.
 2: apply not_eq_sym, Rlt_not_eq, Rplus_lt_reg_r with z; now ring_simplify.
 apply Rinv_lt_contravar; try assumption.
 apply Rmult_lt_0_compat; try apply INRp1_pos.
diff --git a/Lebesgue/nat_compl.v b/Lebesgue/nat_compl.v
index 29ffee294f244c63dc466a8ecfd43e12040e2b40..3c705e20aa458731b9af988d907bd56b844ceda2 100644
--- a/Lebesgue/nat_compl.v
+++ b/Lebesgue/nat_compl.v
@@ -66,7 +66,7 @@ intros f n p H.
 induction n.
 rewrite Nat.le_0_r in H; now rewrite H.
 simpl; case (le_lt_eq_dec p (S n)); try easy; intros Hp.
-apply le_trans with (max_n f n).
+apply Nat.le_trans with (max_n f n).
 apply IHn; lia.
 apply Nat.le_max_r.
 rewrite Hp.
@@ -103,8 +103,7 @@ Qed.
 Lemma lt_mul_S :
   forall N M p, p < S N * S M <-> p < S (pred (S N * S M)).
 Proof.
-intros; rewrite <- S_pred_pos; try easy.
-apply Nat.mul_pos_pos; lia.
+now intros N M p; rewrite Nat.succ_pred.
 Qed.
 
 End Mult_compl.
@@ -123,7 +122,7 @@ destruct N.
 rewrite Nat.pow_1_l; lia.
 destruct M.
 rewrite Nat.pow_0_r; lia.
-apply lt_trans with (S M); try lia.
+apply Nat.lt_trans with (S M); try lia.
 apply Nat.pow_gt_lin_r; lia.
 Qed.
 
diff --git a/Lebesgue/sigma_algebra_R_Rbar.v b/Lebesgue/sigma_algebra_R_Rbar.v
index f66a0073a62050c8d9ae71308e5c3bc16123924c..641eec751cdfcfbcd28742187515ca198491400a 100644
--- a/Lebesgue/sigma_algebra_R_Rbar.v
+++ b/Lebesgue/sigma_algebra_R_Rbar.v
@@ -442,8 +442,7 @@ now apply Rlt_Rminus.
 exists (Z.abs_nat (up (/(x-r)))).
 unfold A; apply Rle_trans with (r+(x-r));[idtac|right; ring].
 apply Rplus_le_compat_l.
-rewrite <- Rinv_involutive.
-2: now apply Rgt_not_eq.
+rewrite <- Rinv_inv.
 apply Rinv_le_contravar.
 now apply Rinv_0_lt_compat.
 apply Rle_trans with (IZR (up (/(x-r)))).
@@ -591,8 +590,7 @@ exists (Z.abs_nat (up (/(r-x)))).
 unfold A; apply Rle_trans with (r-(r-x));[right; ring|idtac].
 apply Rplus_le_compat_l.
 apply Ropp_le_contravar.
-rewrite <- Rinv_involutive.
-2: now apply Rgt_not_eq.
+rewrite <- Rinv_inv.
 apply Rinv_le_contravar.
 now apply Rinv_0_lt_compat.
 apply Rle_trans with (IZR (up (/(r-x)))).
diff --git a/Lebesgue/simple_fun.v b/Lebesgue/simple_fun.v
index 6882841e2c5e3631746f8b5ed728679bee835177..d599d1b438d533becc4db5806b81290fee31f6b9 100644
--- a/Lebesgue/simple_fun.v
+++ b/Lebesgue/simple_fun.v
@@ -32,7 +32,7 @@ Require Import R_compl Rbar_compl sum_Rbar_nonneg.
 Require Import Subset Subset_charac.
 Require Import sigma_algebra sigma_algebra_R_Rbar.
 Require Import measurable_fun.
-Require Import measure.
+Require Import measure logic_compl.
 
 
 Section finite_vals_def.
@@ -1728,10 +1728,9 @@ apply in_eq.
 destruct IHN as (l,Hl).
 exists (S N ::l).
 intros i Hi.
-case (le_lt_or_eq i (S N)); try easy.
-intros Hi'; apply in_cons.
-apply Hl; lia.
-intros Hi'; rewrite Hi'; apply in_eq.
+destruct (ifflr (Nat.lt_eq_cases i (S N))) as [iltSn | ->]; try easy.
+now apply in_cons, Hl; lia.
+now simpl; left.
 (* *)
 intros n.
 assert (C: { l | forall i,
diff --git a/Lebesgue/subset_compl.v b/Lebesgue/subset_compl.v
index 29398c08e4b2710568160df2bee1b1c9053c796b..35f35b6ea7fbb31344e79ec2e2fa61c3a8a538d1 100644
--- a/Lebesgue/subset_compl.v
+++ b/Lebesgue/subset_compl.v
@@ -23,6 +23,7 @@ COPYING file for more details.
 
 From Coq Require Import ClassicalDescription Arith Lia.
 
+Require Import logic_compl.
 
 Section Subset_sequence.
 
@@ -83,6 +84,7 @@ assert (HBm : exists n m, (m <= n)%nat /\ layers m x).
 destruct HBm as [nb [mb [Hmb HBm]]]; now exists mb.
 Qed.
 
+
 (* From Lemma 215 pp. 34-35 *)
 Lemma layers_disjoint :
   (forall n x, A n x -> A (S n) x) ->
@@ -93,9 +95,9 @@ assert (HA' : forall n m x, (n < m)%nat -> A n x -> A m x).
   intros n m x Hnm HAn.
   induction m; try lia.
   apply HA.
-  case (le_lt_or_eq n m); try lia; intros H.
-    apply (IHm H).
-    now rewrite <- H.
+  destruct (ifflr (Nat.lt_eq_cases n m)) as [nltm | ->]; try easy.
+  now apply Nat.lt_succ_r.
+  now apply IHm.
 assert (HBA' : forall n x, layers (S n) x -> A n x -> False).
   intros n x HBSn HAn; now unfold layers in HBSn.
 assert (HBA'' : forall n m x,
@@ -103,7 +105,7 @@ assert (HBA'' : forall n m x,
   intros n m x Hnm HAn HBm.
   apply HBA' with (pred m) x.
   replace (S (pred m)) with m; [ easy | lia ].
-  case (le_lt_or_eq n (pred m)); try lia; intros Hn.
+  case (ifflr (Nat.lt_eq_cases n (pred m))); try lia; intros Hn.
     apply HA' with n; try easy.
     now replace (pred m) with n.
 assert (HB : forall n m x,
diff --git a/Lebesgue/sum_Rbar_nonneg.v b/Lebesgue/sum_Rbar_nonneg.v
index 4c12f570c088d69f774710d148475ee8743b2c59..165029e737b05143fa88fa9b4e9b83edcb9e2166 100644
--- a/Lebesgue/sum_Rbar_nonneg.v
+++ b/Lebesgue/sum_Rbar_nonneg.v
@@ -20,6 +20,7 @@ From Coquelicot Require Import Coquelicot.
 
 Require Import nat_compl list_compl Rbar_compl.
 Require Import Subset_charac.
+Require Import logic_compl.
 
 Open Scope list_scope.
 
@@ -501,11 +502,12 @@ rewrite Hi' in Hui; rewrite Hui.
 rewrite Rbar_plus_comm; apply Rbar_plus_pos_pinfty.
 apply sum_Rbar_ge_0; intros j Hj; apply Hu; lia.
 (* . *)
-destruct (nat_total_order _ _ Hi') as [Hi'' | Hi''].
-apply lt_n_Sm_le in Hi''.
+destruct (ifflr (Nat.lt_gt_cases _ _ )Hi') as [Hi'' | Hi''].
+apply Nat.lt_succ_r in Hi''.
 rewrite IHn; try easy.
 now apply Rbar_plus_pos_pinfty, Hu.
 intros j Hj; apply Hu; lia.
+lia.
 contradict Hi''; lia.
 Qed.
 
@@ -1513,7 +1515,7 @@ trans (sum_Rbar i (fun j => u' (phi j))).
 apply double_series_aux1; try easy.
 intros p q j Hp Hq Hj; apply f_equal with (f := psi) in Hj; rewrite HN1 in Hj.
 rewrite Hj; unfold i.
-apply le_trans with (max_n (fun q' => psi (p, q')) m).
+apply Nat.le_trans with (max_n (fun q' => psi (p, q')) m).
 now apply max_n_correct with (f := fun q' => psi (p, q')).
 now apply max_n_correct with (f := fun p' => max_n (fun q' => psi (p', q')) m).
 (* *)