diff --git a/FEM/Coquelicot_ssr.v b/FEM/Coquelicot_ssr.v
index c595c144061120795e8cc3d5fdabefb7ed1cef51..5b5e4f46eb92dd42abe60c9c15a9cbf027b8b41a 100644
--- a/FEM/Coquelicot_ssr.v
+++ b/FEM/Coquelicot_ssr.v
@@ -3,8 +3,13 @@ Require Import Epsilon_instances choiceType_from_Epsilon.
 From Coquelicot Require Import Coquelicot.
 
 Require Import Rstruct.
+
+Set Warnings "-notation-overridden".
 From mathcomp Require Import ssreflect all_algebra ssrfun.
 From mathcomp Require Import choice eqtype ssrbool.
+Set Warnings "notation-overridden".
+
+Require Import ssr_Coquelicot.
 
 (** Bridge between canonical structures from Coquelicot to math-comp/ssreflect. *)
 
@@ -110,10 +115,10 @@ Proof.
 exact: mult_distr_r.
 Qed.
 
+(*
 About Ring.
-
 Print Canonical Projections Ring.sort.
-
+*)
 (* Next axiom is actually "one != 0", but that statement does not compile... *)
 (* write it as a hypothesis instead of axioms
  *)
@@ -152,13 +157,13 @@ Lemma toto3: right_distributive scal (@plus E).
 Admitted.
 
 Lemma toto4 : forall v : E,
-        {morph scal^~ v : a b / (plus a b) >-> 
+        {morph scal^~ v : a b / (@plus K a b) >-> 
         (plus a b)} .
 Proof.
 intros v a b.
 Admitted.
 
-Require Import ssr_Coquelicot.
+
 
 Definition ModuleSpace_lmodType_Mixin :=
   (@LmodMixin (Ring_ringType K) 
@@ -227,10 +232,10 @@ Canonical Structure matrix_ModuleSpace :=
     (ModuleSpace.Class K (zmodType_AbelianGroup (matrix_zmodType (Ring_ringType K) m n))
       _ matrix_ModuleSpace_mixin)
     (zmodType_AbelianGroup (matrix_zmodType (Ring_ringType K) m n)).
-
+(*
 Print Canonical Projections matrix.
-
 Print Canonical Projections .
+*)
 
 End matrix_ModuleSpace.
 
diff --git a/FEM/Epsilon_instances.v b/FEM/Epsilon_instances.v
index 04fead0f3b279f885526c115c53d8d10485e1f75..e761d57477f7a806f7b458892b7bab6d10bed959 100644
--- a/FEM/Epsilon_instances.v
+++ b/FEM/Epsilon_instances.v
@@ -22,8 +22,10 @@ COPYING file for more details.
     See files choiceType_from_Epsilon.v, Rstruct.v, and signal.v.
 **)
 
+Set Warnings "-notation-overridden".
 From mathcomp
 Require Import ssreflect ssralg vector.
+Set Warnings "notation-overridden".
 
 Require Import Rdefinitions.
 
@@ -73,4 +75,4 @@ apply: epsilon_statement.
 exact: (inhabits (fun _ => GRing.zero _)).
 Qed.
 
- *)
\ No newline at end of file
+ *)
diff --git a/FEM/Finite_dim.v b/FEM/Finite_dim.v
index a9e74db70ed608f076cf4b35750c4e10b684f80c..7cacfac20a211a10833bb7292292dd459e451654 100644
--- a/FEM/Finite_dim.v
+++ b/FEM/Finite_dim.v
@@ -3,12 +3,10 @@ From Coq Require Import PropExtensionality FunctionalExtensionality.
 
 From Coquelicot Require Import Coquelicot.
 
+Set Warnings "-notation-overridden".
 From mathcomp Require Import ssrbool ssrnat fintype bigop vector.
-
-Add LoadPath "../LM" as LM.
 From LM Require Import check_sub_structure.
-
-Add LoadPath "../Lebesgue" as Lebesgue.
+Set Warnings "notation-overridden".
 
 From Lebesgue Require Import Function Subset FinBij.
 
@@ -412,7 +410,7 @@ unfold dual_basis.
 destruct (excluded_middle_informative _) as [Hx | Hx].
 destruct (span_strong_ex _ _ _) as [L' HL'].
 assert (T:L=L'); [idtac| rewrite T; easy].
-apply is_free_has_uniq_decomp with (B:=B); try easy.
+apply (is_free_has_uniq_decomp B); try easy.
 apply HB.
 rewrite <- H; easy.
 contradict Hx.
diff --git a/FEM/Makefile b/FEM/Makefile
index d3efbf2bd1f03967df50bc392cab72269e7a2e8e..5300c332ba15b67b5091cf508be8777d1e3137ed 100644
--- a/FEM/Makefile
+++ b/FEM/Makefile
@@ -7,7 +7,7 @@
 ##         #     GNU Lesser General Public License Version 2.1          ##
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
-## GNUMakefile for Coq 8.15.0
+## GNUMakefile for Coq 8.14.0
 
 # For debugging purposes (must stay here, don't move below)
 INITIAL_VARS := $(.VARIABLES)
@@ -90,7 +90,6 @@ else
 STDTIME?=command time -f $(TIMEFMT)
 endif
 
-COQBIN?=
 ifneq (,$(COQBIN))
 # add an ending /
 COQBIN:=$(COQBIN)/
@@ -169,7 +168,7 @@ destination_path = $(if $(DESTDIR),$(DESTDIR)/$(call windrive_path,$(1)),$(1))
 
 # Installation paths of libraries and documentation.
 COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib)
-COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/coq/user-contrib)
+COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/user-contrib)
 COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable?
 
 ########## End of parameters ##################################################
@@ -257,7 +256,7 @@ COQDOCLIBS?=$(COQLIBS_NOML)
 # The version of Coq being run and the version of coq_makefile that
 # generated this makefile
 COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
-COQMAKEFILE_VERSION:=8.15.0
+COQMAKEFILE_VERSION:=8.14.0
 
 # COQ_SRC_SUBDIRS is for user-overriding, usually to add
 # `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for
@@ -759,7 +758,7 @@ else
 TIMING_EXTRA =
 endif
 
-$(VOFILES): %.vo: %.v | $(VDFILE)
+$(VOFILES): %.vo: %.v
 	$(SHOW)COQC $<
 	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA)
 ifeq ($(COQDONATIVE), "yes")
diff --git a/FEM/Rstruct.v b/FEM/Rstruct.v
index d25d8dc27cf041fb298b7e02423ccbcf26352a9e..1f9cc36f3a865cd7945df065818a23d48e3707f7 100644
--- a/FEM/Rstruct.v
+++ b/FEM/Rstruct.v
@@ -36,10 +36,12 @@ Require Import (* Epsilon *) FunctionalExtensionality ProofIrrelevance Lra.
 
 Require Import Rdefinitions Raxioms RIneq Rbasic_fun Rpow_def.
 Require Import Epsilon FunctionalExtensionality.
+Set Warnings "-notation-overridden".
 Require Import mathcomp.ssreflect.ssreflect mathcomp.ssreflect.ssrfun mathcomp.ssreflect.ssrbool mathcomp.ssreflect.eqtype mathcomp.ssreflect.ssrnat.
 Require Import mathcomp.ssreflect.choice mathcomp.ssreflect.bigop mathcomp.algebra.ssralg.
 Require Import mathcomp.algebra.ssrnum.
 Require Import mathcomp.algebra.vector.
+Set Warnings "notation-overridden".
 
 
 Set Implicit Arguments.
diff --git a/FEM/_CoqProject b/FEM/_CoqProject
index edaaae53b9ce8d16ea51f1dfbf1638a9a4244a9e..c2c029767c2c3e58711a23e9b37f98bf13b72bae 100644
--- a/FEM/_CoqProject
+++ b/FEM/_CoqProject
@@ -1,4 +1,6 @@
 -R . FEM
+-R ../LM LM
+-R ../Lebesgue Lebesgue
 -arg -w
 -arg -ambiguous-paths
 
diff --git a/FEM/bijective.v b/FEM/bijective.v
index 89c1bb2fd5751c75aabf8f2ca0adb7b69532e56d..1e5a5898422d9e93d059ee5ada2aa77d602dbe2b 100644
--- a/FEM/bijective.v
+++ b/FEM/bijective.v
@@ -2,10 +2,8 @@ From Coq Require Import FunctionalExtensionality ClassicalDescription ClassicalC
 From Coq Require Import  Morphisms.
 From Coq Require Import Arith Lia Reals Lra.
 
-Add LoadPath "../LM" as LM.
 From LM Require Import linear_map.
 
-Add LoadPath "../Lebesgue" as Lebesgue.
 From Lebesgue Require Import Function.
 
 Section Funbij0.
diff --git a/FEM/choiceType_from_Epsilon.v b/FEM/choiceType_from_Epsilon.v
index 28acc35f5c32b6dd9c4d13af63ecdae45e40e6f4..cd71364a922b4f980028187b13d8caedf6f73392 100644
--- a/FEM/choiceType_from_Epsilon.v
+++ b/FEM/choiceType_from_Epsilon.v
@@ -21,8 +21,10 @@ COPYING file for more details.
     the type signal.
 **)
 
+Set Warnings "-notation-overridden".
 From mathcomp
 Require Import ssreflect ssrbool ssrfun choice.
+Set Warnings "notation-overridden".
 
 Require Import FunctionalExtensionality.
 
diff --git a/FEM/comb_lin.v b/FEM/comb_lin.v
index ce54dccf3e5ac7ceb373c6eb3c85495a1a1769a5..140a9496a0a80022f9a6eb73a67d4f60eca217f5 100644
--- a/FEM/comb_lin.v
+++ b/FEM/comb_lin.v
@@ -2,12 +2,13 @@ From Coq Require Import Lia Reals Lra FunctionalExtensionality.
 
 From Coquelicot Require Import Coquelicot.
 
+Set Warnings "-notation-overridden".
 From mathcomp Require Import bigop vector all_algebra fintype tuple ssrfun.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 From mathcomp Require Import seq path ssralg div tuple finfun.
 
-Add LoadPath "../LM" as LM.
 From LM Require Import linear_map.
+Set Warnings "notation-overridden".
 
 Notation "''' E ^ n" := ('I_n -> E)
   (at level 8, E at level 2, n at level 2, format "''' E ^ n").
diff --git a/FEM/finite_element.v b/FEM/finite_element.v
index f92f02656c11cbd2077afd61aad705e626a62ccf..391d768d7b5cae17f120b89390e81bc824390883 100644
--- a/FEM/finite_element.v
+++ b/FEM/finite_element.v
@@ -15,20 +15,26 @@ COPYING file for more details.
 *)
 
 From Coq Require Import Lia Reals Lra.
+
+Set Warnings "-notation-overridden".
 From Coq Require Import PropExtensionality FunctionalExtensionality ClassicalDescription ClassicalChoice ClassicalEpsilon.
+Set Warnings "notation-overridden".
 From Coq Require Import List.
 
 From Coquelicot Require Import Coquelicot.
 
 Require Import Rstruct.
+(*Note that all_algebra prevents the use of ring *)
+Set Warnings "-notation-overridden".
 From mathcomp Require Import bigop vector ssrfun tuple fintype ssralg.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat.
 From mathcomp Require Import seq path poly mxalgebra matrix.
+Set Warnings "notation-overridden".
 
-Add LoadPath "../LM" as LM.
+Set Warnings "-notation-overridden".
 From LM Require Import linear_map check_sub_structure.
+Set Warnings "notation-overridden".
 
-Add LoadPath "../Lebesgue" as Lebesgue.
 From Lebesgue Require Import Function Subset LInt_p FinBij.
 
 Require Import kronecker poly_Lagrange.
@@ -892,7 +898,12 @@ apply comb_lin_ext; intros i.
 f_equal; apply theta_cur_correct.
 Qed.
 
+<<<<<<< HEAD
 End FE_Current_Def.
+=======
+*)
+End FE_Reference_Def.
+>>>>>>> pr_compat_816
 
 Section FE_Lagrange.
 
@@ -1011,4 +1022,4 @@ Proof.
 intros v.
 Admitted.
 *)
-End FE_Lagrange.
\ No newline at end of file
+End FE_Lagrange.
diff --git a/FEM/geometry.v b/FEM/geometry.v
index 23cadd9333725cb0acaf9d3fcaa9da2da4fa3b6b..17781b76241ac1a42690b8e3221ad49e9b40f0dd 100644
--- a/FEM/geometry.v
+++ b/FEM/geometry.v
@@ -5,8 +5,10 @@ From Coquelicot Require Import Coquelicot.
 
 From mathcomp Require Import bigop vector all_algebra fintype tuple ssrfun.
 Require Import Rstruct.
+Set Warnings "-notation-overridden".
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 From mathcomp Require Import seq path.
+Set Warnings "notation-overridden".
 
 Add LoadPath "../LM" as LM.
 Add LoadPath "../Lebesgue" as Lebesgue.
diff --git a/FEM/kronecker.v b/FEM/kronecker.v
index 93a79bd48457a4f2d85f264511a71da11309f90e..07d3661f6113534057ab71496a3eb383c7bf6bdb 100644
--- a/FEM/kronecker.v
+++ b/FEM/kronecker.v
@@ -5,13 +5,11 @@ From Coq Require Import List.
 From Coquelicot Require Import Coquelicot.
 
 Require Import Rstruct.
+Set Warnings "-notation-overridden".
 From mathcomp Require Import bigop vector all_algebra fintype tuple ssrfun.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat.
 From mathcomp Require Import seq path.
-
-Add LoadPath "../LM" as LM.
-
-Add LoadPath "../Lebesgue" as Lebesgue.
+Set Warnings "notation-overridden".
 
 Require Import comb_lin.
 
diff --git a/FEM/poly_Lagrange.v b/FEM/poly_Lagrange.v
index a6bb036ee0b0493570b3e39cedb511cbc673f466..862ab3f5797c61a6b9d4e18388978687e97dfb4f 100644
--- a/FEM/poly_Lagrange.v
+++ b/FEM/poly_Lagrange.v
@@ -6,14 +6,15 @@ From Coquelicot Require Import Coquelicot.
 
 Require Import Rstruct.
 
+Set Warnings "-notation-overridden".
 From mathcomp Require Import bigop vector ssrfun tuple fintype ssralg.
 From mathcomp Require Import ssrbool eqtype ssrnat.
-From mathcomp Require Import seq path poly matrix ssreflect.
+From mathcomp Require Import seq path poly matrix ssreflect
+Set Warnings "notation-overridden".
 
-Add LoadPath "../LM" as LM.
 From LM Require Import linear_map check_sub_structure.
 
-Add LoadPath "../Lebesgue" as Lebesgue.
+
 From Lebesgue Require Import Function Subset LInt_p FinBij.
 
 Require Import kronecker.
@@ -209,6 +210,7 @@ intros.
 unfold comb_lin.
 Admitted.
 
+<<<<<<< HEAD
 End Poly_Lagrange_Quad.
 
 Section LagPQ.
@@ -222,4 +224,7 @@ unfold LagQ1.
 Admitted.
 
 
-End LagPQ.
\ No newline at end of file
+End LagPQ.
+=======
+End Poly_Lagrange_basis.
+>>>>>>> pr_compat_816
diff --git a/FEM/sandbox.v b/FEM/sandbox.v
index 9ffe4c1b48ef64c81d4effbf3203f991bcb196e4..30a5acb5bc9ae8711cb7318f3469155dc20f8af2 100644
--- a/FEM/sandbox.v
+++ b/FEM/sandbox.v
@@ -19,17 +19,18 @@ From Coq Require Import PropExtensionality FunctionalExtensionality ClassicalDes
 From Coq Require Import List.
 From Coquelicot Require Import Coquelicot.
 
-Add LoadPath "../Lebesgue" as Lebesgue.
 From Lebesgue Require Import Function LInt_p FinBij.
 
-Add LoadPath "../LM" as LM.
 From LM Require Import linear_map check_sub_structure.
 
 Require Import Rstruct.
+
+Set Warnings "-notation-overridden".
 From mathcomp Require Import bigop vector ssrfun tuple fintype ssralg matrix.
 (*Note that all_algebra prevents the use of ring *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 From mathcomp Require Import seq path poly.
+Set Warnings "notation-overridden".
 
 From SsrMultinomials Require Import mpoly.
 
diff --git a/FEM/ssr_Coquelicot.v b/FEM/ssr_Coquelicot.v
index d76a484abfe1680a8c940f2644f0aa10f7ea2351..6b5572bcd65f23db40281eaf5e96ca83250f1edd 100644
--- a/FEM/ssr_Coquelicot.v
+++ b/FEM/ssr_Coquelicot.v
@@ -1,7 +1,10 @@
 From Coquelicot Require Import Coquelicot.
 
 Require Import Rstruct.
+
+Set Warnings "-notation-overridden".
 From mathcomp Require Import ssreflect all_algebra ssrfun eqtype.
+Set Warnings "notation-overridden".
 
 Local Open Scope ring_scope.
 
diff --git a/LM/R_compl.v b/LM/R_compl.v
index 04d53c241b4cfae6914701e02a586551f381c5d2..0b9bc0aa417c96e9e697a6e8cc639508ab11eac5 100644
--- a/LM/R_compl.v
+++ b/LM/R_compl.v
@@ -148,10 +148,9 @@ case (Req_dec x 0); intros Hx.
 rewrite Hx; now left.
 destruct H2.
 left; now apply Rinv_lt_cancel.
-right; rewrite <- Rinv_involutive.
-2: now apply Rgt_not_eq.
+right; rewrite <- Rinv_inv.
 rewrite H.
-now apply sym_eq, Rinv_involutive.
+now apply sym_eq, Rinv_inv.
 Qed.
 
 Lemma Rlt_R1_pow: forall x n, 0 <= x < 1 -> (0 < n)%nat -> x ^ n < 1.
@@ -163,7 +162,7 @@ apply Rlt_0_1.
 apply Rinv_lt_cancel.
 apply Rlt_0_1.
 rewrite Rinv_1.
-rewrite Rinv_pow; try assumption.
+rewrite <-pow_inv; try assumption.
 apply Rlt_pow_R1; try assumption.
 rewrite <- Rinv_1.
 apply Rinv_lt_contravar; try assumption.
@@ -177,7 +176,7 @@ Proof.
 intros x m n (Hx1,Hx2) H.
 apply Rinv_le_cancel.
 now apply pow_lt.
-rewrite 2!Rinv_pow; try now apply Rgt_not_eq.
+rewrite <-2!pow_inv; try now apply Rgt_not_eq.
 apply Rle_pow; try assumption.
 rewrite <- Rinv_1.
 apply Rinv_le_contravar; try assumption.
diff --git a/LM/check_sub_structure.v b/LM/check_sub_structure.v
index d3c2480b6dbbe897a347227a9d36ceffdc57d571..a1f5e2720123a501ab9958acf0d8075a7432b832 100644
--- a/LM/check_sub_structure.v
+++ b/LM/check_sub_structure.v
@@ -139,14 +139,14 @@ Definition Sg_MAbelianGroup_mixin :=
   AbelianGroup.Mixin Sg Sg_Mplus Sg_opp Sg_zero Sg_plus_comm
    Sg_plus_assoc Sg_plus_zero_r Sg_plus_opp_r.
 
-Canonical Sg_MAbelianGroup :=
+Definition Sg_MAbelianGroup :=
   AbelianGroup.Pack Sg (Sg_MAbelianGroup_mixin) (@Sg _ P).
 
 Definition Sg_ModuleSpace_mixin :=
 ModuleSpace.Mixin R_Ring (Sg_MAbelianGroup)
    _ Sg_mult_assoc Sg_mult_one_l Sg_mult_distr_l Sg_mult_distr_r.
 
-Canonical Sg_ModuleSpace :=
+Definition Sg_ModuleSpace :=
   ModuleSpace.Pack R_Ring Sg (ModuleSpace.Class _ _ _ Sg_ModuleSpace_mixin) (@Sg G P).
 
 End Submodules.
diff --git a/LM/finitedim.v b/LM/finitedim.v
index 13a2e1d6f306a624e83a258caa9a28d629fec10e..78ec79afc62cd470f92994b9c6b5c61ba3154bc0 100644
--- a/LM/finitedim.v
+++ b/LM/finitedim.v
@@ -104,7 +104,7 @@ replace i with 0%nat by auto with zarith.
 rewrite sum_O.
 simpl.
 now rewrite scal_one.
-intros Hi; case (le_lt_or_eq _ _ Hi); intros Hi2.
+intros Hi; destruct (Nat.lt_eq_cases i (S m)) as [[i_inf | i_eq]]; try easy.
 rewrite IHm.
 2: auto with zarith.
 rewrite sum_Sn.
@@ -112,11 +112,11 @@ replace (scal (match (eq_nat_dec i (S m)) with
   | left _ => 1 | _ => 0 end) (B (S m))) with (@zero E).
 apply sym_eq, plus_zero_r.
 case (eq_nat_dec i (S m)); intros T.
-contradict Hi2; auto with zarith.
+contradict i_inf; auto with zarith.
 now rewrite scal_zero_l.
 rewrite <- (plus_zero_l (B i)).
 rewrite sum_Sn.
-rewrite Hi2; f_equal.
+rewrite i_eq; f_equal.
 apply sym_eq.
 apply: sum_n_eq_zero.
 intros k Hk.
@@ -125,7 +125,7 @@ intros Hk2; contradict Hk; auto with zarith.
 intros _; apply: scal_zero_l.
 case eq_nat_dec.
 intros _; now rewrite scal_one.
-intros H; now contradict H.
+intros Hcontra. now contradict Hcontra.
 Qed.
 
 Lemma phi_B: (0 < dim)%nat -> forall i:nat, (i <= dim-1)%nat ->
@@ -163,11 +163,10 @@ auto with zarith.
 intros T1.
 case (Req_dec (f (B (S n -1))) 0); intros T2.
 right; intros i Hi.
-case (le_lt_or_eq i (S n - 1)).
+destruct (Nat.lt_eq_cases i (S n - 1)) as [[Hi2 | Hi2] _].
 auto with zarith.
-intros Hi2.
 apply T1. auto with zarith.
-intros Hi2; rewrite Hi2; assumption.
+rewrite Hi2; assumption.
 left.
 exists (S n - 1)%nat; split; try assumption.
 auto with zarith.
diff --git a/LM/fixed_point.v b/LM/fixed_point.v
index 7f4bd668bf1d0c8126c843ef45d6d701f01c6039..d6ff9bf303646564c4b9b7518cd26ce364041c20 100644
--- a/LM/fixed_point.v
+++ b/LM/fixed_point.v
@@ -105,7 +105,7 @@ Proof.
 intros f a k p m D H1 H2 H3 H4.
 case_eq m.
 (* *)
-intros _; rewrite plus_0_r.
+intros _; rewrite Nat.add_0_r.
 assert (L:(0 < k ^ p / (1 - k) * D)).
 apply Rmult_lt_0_compat; trivial.
 apply Rdiv_lt_0_compat.
@@ -184,7 +184,7 @@ Proof.
 intros a k p m n D (H1,H1') H2 Phi_a H3 H4 Hp Hm Hn.
 case H1; intros P.
 (* *)
-case (le_or_lt p m); intros H5.
+case (Nat.le_gt_cases p m); intros H5.
 (* . *)
 replace m with (p+(m-p))%nat.
 apply ball_le with (k^p/(1-k) *D).
@@ -197,7 +197,7 @@ apply Rle_pow_le; try assumption.
 split; try left; try assumption.
 apply dist_iter; try assumption.
 split; assumption.
-now apply le_plus_minus_r.
+now rewrite Nat.add_comm, Nat.sub_add.
 (* . *)
 apply ball_sym.
 replace p with (m+(p-m))%nat.
@@ -211,7 +211,7 @@ apply Rle_pow_le; try assumption.
 split; try left; assumption.
 apply dist_iter; try assumption.
 split; assumption.
-now apply le_plus_minus_r, lt_le_weak.
+rewrite Nat.add_comm, Nat.sub_add; [reflexivity | apply Nat.lt_le_incl; assumption].
 (* *)
 apply ball_le with 0.
 rewrite <- P.
@@ -219,8 +219,8 @@ rewrite pow_i; try assumption.
 right; unfold Rdiv; ring.
 apply dist_iter_aux_zero; try assumption.
 now rewrite P.
-now apply lt_le_trans with n.
-now apply lt_le_trans with n.
+now apply Nat.lt_le_trans with n.
+now apply Nat.lt_le_trans with n.
 Qed.
 
 End iter_dist.
@@ -403,11 +403,11 @@ intros P Q (N1,H1) (N2,H2).
 exists (max N1 N2).
 intros n Hn; split.
 apply H1.
-apply le_trans with (2:=Hn).
-apply Max.le_max_l.
+apply Nat.le_trans with (2:=Hn).
+apply Nat.le_max_l.
 apply H2.
-apply le_trans with (2:=Hn).
-apply Max.le_max_r.
+apply Nat.le_trans with (2:=Hn).
+apply Nat.le_max_r.
 intros P Q H (N,HN).
 exists N.
 intros n Hn.
@@ -746,7 +746,7 @@ Proof.
 intros f P a k p m D H1 H2 HH H3 H4.
 case_eq m.
 (* *)
-intros _; rewrite plus_0_r.
+intros _; rewrite Nat.add_0_r.
 assert (L:(0 < k ^ p / (1 - k) * D)).
 apply Rmult_lt_0_compat; trivial.
 apply Rdiv_lt_0_compat.
@@ -825,7 +825,7 @@ Proof.
 intros a k p m n D (H1,H1') H2 Phi_a H3 H4 Hp Hm Hn.
 case H1; intros P0.
 (* *)
-case (le_or_lt p m); intros H5.
+case (Nat.le_gt_cases p m); intros H5.
 (* . *)
 replace m with (p+(m-p))%nat.
 apply ball_le with (k^p/(1-k) *D).
@@ -842,7 +842,7 @@ intros p0.
 apply phi_iter_f.
 trivial.
 trivial.
-now apply le_plus_minus_r.
+now rewrite Nat.add_comm, Nat.sub_add.
 (* . *)
 apply ball_sym.
 replace p with (m+(p-m))%nat.
@@ -858,7 +858,7 @@ apply dist_iter_phi with phi; try assumption.
 split; assumption.
 intros p0.
 apply phi_iter_f; trivial.
-now apply le_plus_minus_r, lt_le_weak.
+now rewrite Nat.add_comm, Nat.sub_add; [idtac | apply Nat.lt_le_incl].
 (* *)
 apply ball_le with 0.
 rewrite <- P0.
@@ -866,8 +866,8 @@ rewrite pow_i; try assumption.
 right; unfold Rdiv; ring.
 apply dist_iter_aux_zero_phi; try assumption.
 now rewrite P0.
-now apply lt_le_trans with n.
-now apply lt_le_trans with n.
+now apply Nat.lt_le_trans with n.
+now apply Nat.lt_le_trans with n.
 Qed.
 
 End iter_dist_sub.
@@ -979,11 +979,11 @@ intros P Q (N1,H1) (N2,H2).
 exists (max N1 N2).
 intros n Hn; split.
 apply H1.
-apply le_trans with (2:=Hn).
-apply Max.le_max_l.
+apply Nat.le_trans with (2:=Hn).
+apply Nat.le_max_l.
 apply H2.
-apply le_trans with (2:=Hn).
-apply Max.le_max_r.
+apply Nat.le_trans with (2:=Hn).
+apply Nat.le_max_r.
 intros P Q H (N,HN).
 exists N.
 intros n Hn.
diff --git a/LM/hierarchyD.v b/LM/hierarchyD.v
index e1f9fbcb53e7a055ce0f19c217c633e54e557b1e..757cceec16755aa343def449c881d1dc730781b8 100644
--- a/LM/hierarchyD.v
+++ b/LM/hierarchyD.v
@@ -189,9 +189,9 @@ Proof.
   case: (HFc1 (pos_div_2 eps)) => {HFc1} P ; simpl ; case => HP H0.
   apply filter_imp with (2 := HP).
   move => g Hg t.
-  move: (fun h => H0 g h Hg) => {H0} H0.
-  move: (H t (pos_div_2 eps)) ; simpl => {H} H.
-  unfold Fr in H ; generalize (filter_and _ _ H HP) => {H} H.
+  move: (fun h => H0 g h Hg) => {H0} => H0.
+  move: (H t (pos_div_2 eps)) ; simpl => {H} => H.
+  unfold Fr in H ; generalize (filter_and _ _ H HP) => {H} => H.
   apply filter_ex in H ; case: H => h H.
   rewrite (double_var eps).
   apply ball_triangle with (h t).
@@ -353,9 +353,6 @@ Canonical CompleteNormedModule_CompleteNormedModuleD :=
 
 End CNM_is_CNMD.
 
-Canonical R_CompleteNormedModuleD :=
-  @CompleteNormedModule_CompleteNormedModuleD R_CompleteNormedModule.
-
 (** Clm is CompleteNormedModuleD *)
 
 Section clm_complete.
diff --git a/LM/lax_milgram.v b/LM/lax_milgram.v
index 53cb357f8461c87bcca621b80543526ef7871bf8..0b7e6681c26b8278dd96d5809bcfe7f6e1955abc 100644
--- a/LM/lax_milgram.v
+++ b/LM/lax_milgram.v
@@ -1209,13 +1209,8 @@ apply Hp.
 rewrite Rsqr_mult.
 assert (Hqd : (alpha * alpha) / (C * C)
        = (alpha / C)²).
-rewrite Rsqr_div.
+rewrite Rsqr_div'.
 reflexivity.
-apply Rgt_not_eq.
-apply Rlt_gt.
-apply Rlt_le_trans with alpha.
-apply Halpha.
-apply Halpha.
 rewrite <- Hqd.
 rewrite Rplus_comm.
 rewrite <- Rplus_assoc.
@@ -1272,13 +1267,13 @@ apply Rsqr_le_abs_1.
 unfold Rabs.
 destruct (Rcase_abs alpha).
 absurd (0 < alpha); trivial.
-apply Rle_not_lt.
+apply Rle_not_gt.
 intuition.
 trivial.
 apply Halpha.
 destruct (Rcase_abs C).
 absurd (0 < C); trivial.
-apply Rle_not_lt.
+apply Rle_not_gt.
 intuition.
 trivial.
 apply Rlt_le_trans with alpha.
@@ -1395,7 +1390,7 @@ apply Hp.
 rewrite Rsqr_mult.
 assert (Hqd : (alpha * alpha) / (C * C)
        = (alpha / C)²).
-rewrite Rsqr_div.
+rewrite Rsqr_div'.
 reflexivity.
 trivial.
 rewrite <- Hqd.
@@ -1755,7 +1750,7 @@ simpl.
 unfold Rabs.
 destruct (Rcase_abs r).
 absurd (0 < r).
-apply Rle_not_lt.
+apply Rle_not_gt.
 intuition.
 apply Hr.
 apply Hr.
diff --git a/LM/logic_tricks.v b/LM/logic_tricks.v
index 5190454a9d39b65b13274bfcde13f434cb72e310..e4b0a1145106cb2b447c458338eaf83b8f72b913 100644
--- a/LM/logic_tricks.v
+++ b/LM/logic_tricks.v
@@ -118,17 +118,17 @@ 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.
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..64f08367008ce0fc34bf09fbb8248c41439a62b2 100644
--- a/Lebesgue/R_compl.v
+++ b/Lebesgue/R_compl.v
@@ -18,10 +18,59 @@ 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.
 
+(* pris de la lib std en attendant 8.16 pour tout le monde *)
 
-Section R_ring_compl.
+Lemma Rinv_1 : / 1 = 1.
+Proof.
+  field.
+Qed.
+
+Lemma Rinv_0 : / 0 = 0.
+Proof.
+rewrite RinvImpl.Rinv_def.
+case Req_appart_dec.
+- easy.
+- intros [H|H] ; elim Rlt_irrefl with (1 := H).
+Qed.
+
+Lemma Rinv_inv r : / / r = r.
+Proof.
+destruct (Req_dec r 0) as [->|H].
+- rewrite Rinv_0.
+  apply Rinv_0.
+- now field.
+Qed.
+
+Lemma Rinv_mult r1 r2 : / (r1 * r2) = / r1 * / r2.
+Proof.
+destruct (Req_dec r1 0) as [->|H1].
+- rewrite Rinv_0, 2!Rmult_0_l.
+  apply Rinv_0.
+- destruct (Req_dec r2 0) as [->|H2].
+  + rewrite Rinv_0, 2!Rmult_0_r.
+    apply Rinv_0.
+  + now field.
+Qed.
+
+Lemma pow_inv x n : (/ x)^n = / x^n.
+Proof.
+induction n as [|n IH] ; simpl.
+- apply eq_sym, Rinv_1.
+- rewrite Rinv_mult.
+  now apply f_equal.
+Qed.
+
+Lemma Rsqr_div' x y : Rsqr (x / y) = Rsqr x / Rsqr y.
+Proof.
+  unfold Rsqr, Rdiv.
+  rewrite Rinv_mult.
+  ring.
+Qed.
 
+(* fin des lemmes pris de 8.16 *)
 (** Complements on ring operations Rplus and Rmult. **)
 
 Lemma Rplus_not_eq_compat_l : forall r r1 r2, r1 <> r2 -> r + r1 <> r + r2.
@@ -246,9 +295,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 +324,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 +718,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 +1143,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 +1174,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 +1188,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 +1203,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 +1225,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 +1241,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 +1259,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 +1279,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_Rbar.v b/Lebesgue/Subset_Rbar.v
index 48e863e195e4bccfb4f07497d0313f45bfbe95fe..bdff7bf088217ae1b91dc71374716f5fab9e2fab 100644
--- a/Lebesgue/Subset_Rbar.v
+++ b/Lebesgue/Subset_Rbar.v
@@ -474,17 +474,17 @@ intros B [[[a HB] | [HB | HB]] | [[a HB] | [HB | HB]]];
     generalize HB; clear HB; Rbar_interval_full_unfold; intros [HB1 HB2];
     destruct (in_dec B a) as [Ha | Ha].
 (* . *)
-rewrite subset_ext with (B := fun y => Rbar_le y a); try now apply RbR_ge.
+rewrite (subset_ext _ (fun y => Rbar_le y a)); try now apply RbR_ge.
 intros; split; auto; rewrite Rbar_le_equiv; intros [Hy | Hy]; try rewrite Hy; auto.
 (* . *)
-rewrite subset_ext with (B := Rbar_gt a); try apply RbR_gt; try easy.
+rewrite (subset_ext _ (Rbar_gt a)); try apply RbR_gt; try easy.
 intros; split; auto; intros Hy; generalize (HB2 _ Hy); rewrite Rbar_le_equiv.
 intros [HB2a | HB2a]; try easy; rewrite HB2a in Hy; contradiction.
 (* . *)
-rewrite subset_ext with (B := Rbar_le a); try now apply RbR_le.
+rewrite (subset_ext _ (Rbar_le a)); try now apply RbR_le.
 intros; split; auto; rewrite Rbar_le_equiv; intros [Hy | Hy]; try rewrite <- Hy; auto.
 (* . *)
-rewrite subset_ext with (B := Rbar_lt a); try apply RbR_lt; try easy.
+rewrite (subset_ext _ (Rbar_lt a)); try apply RbR_lt; try easy.
 intros; split; auto; intros Hy; generalize (HB2 _ Hy); rewrite Rbar_le_equiv.
 intros [HB2a | HB2a]; try easy; rewrite <- HB2a in Hy; contradiction.
 Qed.
@@ -844,7 +844,7 @@ assert (Hfm2 : fm <= em) by apply Rmin_l.
 pose (b := tan (- (PI / 2) + fm)).
 (* *)
 apply RbSO_winf.
-rewrite subset_ext with (B := union (up_id (down B)) (Rbar_gt b)).
+rewrite (subset_ext _ (union (up_id (down B)) (Rbar_gt b))).
 apply RbSOW_one; [apply open_Rbar_R | apply RbRO_gt]; easy.
 intros y; split; intros Hy.
 (* . *)
@@ -877,7 +877,7 @@ assert (Hfp2 : fp <= ep) by apply Rmin_l.
 pose (a := tan (PI / 2 - fp)).
 (* *)
 apply RbSO_winf.
-rewrite subset_ext with (B := union (up_id (down B)) (Rbar_lt a)).
+rewrite (subset_ext _ (union (up_id (down B)) (Rbar_lt a))).
 apply RbSOW_one; [apply open_Rbar_R | apply RbRO_lt]; easy.
 intros y; split; intros Hy.
 (* . *)
@@ -917,8 +917,8 @@ assert (Hfp1 : - (PI / 2) < PI / 2 - fp < PI / 2) by lra.
 assert (Hfp2 : fp <= ep) by apply Rmin_l.
 pose (a := tan (PI / 2 - fp)).
 (* *)
-apply RbSO_winf; rewrite subset_ext with
-    (B := union (union (up_id (down B)) (Rbar_gt b)) (Rbar_lt a)).
+apply RbSO_winf; rewrite (subset_ext _
+    (union (union (up_id (down B)) (Rbar_gt b)) (Rbar_lt a))).
 apply RbSOW_two, open_Rbar_R; easy.
 intros y; split; intros Hy.
 (* . *)
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..0e03e53f54e94866c35a0c7c7c9010acbf86e690 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 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..3060e5cb31466d32abc43fbc7d66b3d355e3dfde 100644
--- a/Lebesgue/countable_sets.v
+++ b/Lebesgue/countable_sets.v
@@ -17,144 +17,96 @@ COPYING file for more details.
 From Coq Require Import Even ZArith Qreals Reals.
 
 Require Import logic_compl. (* For strong_induction. *)
-
+Require Import Lia.
 
 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.
-Qed.
-
-Lemma Zabs_nat_Zopp : forall z, Z.abs_nat (-z) = Z.abs_nat z.
-Proof.
-intros z; destruct z; easy.
+apply Nat.mul_lt_mono_pos_l with (p:=2%nat); try (constructor; easy).
+destruct (Nat.even b) eqn:parity.
+- apply Nat.even_spec in parity as [b' ->].
+  rewrite Nat.div2_double; try easy.
+  apply (Nat.lt_trans _ (2 * a + 1) _); try easy.
+  now rewrite Nat.add_1_r; constructor.
+- assert (odd_b : Nat.odd b = true) by now unfold Nat.odd; rewrite parity.
+  apply Nat.odd_spec in odd_b as [b' ->].
+  rewrite Nat.add_1_r, Nat.div2_succ_double.
+  now rewrite (Nat.add_lt_mono_r _ _ 1).
 Qed.
 
 
 Section Z_countable.
-
+Open Scope nat_scope.
 Definition bij_ZN : Z -> nat :=
   fun z =>  match Z_lt_le_dec z 0 with
-    | right _ => (2 * Z.abs_nat z)%nat
-    | left _ => (2 * Z.abs_nat z - 1)%nat
+    | right _ => (2 * Z.abs_nat z)
+    | left _ => (2 * Z.abs_nat z - 1)
     end.
 
 Definition bij_NZ : nat -> Z :=
-  fun n => match even_odd_dec n with
-    | left _ => (Z.of_nat (Nat.div2 n))%Z
-    | right _ => (- Z.of_nat (Nat.div2 (n + 1)))%Z
+  fun n => match Nat.even n with
+    | true => (Z.of_nat (Nat.div2 n))%Z
+    | false => (- Z.of_nat (Nat.div2 (n + 1)))%Z
     end.
 
 Lemma bij_NZN : forall z, bij_NZ (bij_ZN z) = z.
 Proof.
 intros z; unfold bij_ZN.
-case (Z_lt_le_dec z 0); intros H1.
-assert (H:(0 < Z.abs_nat z)%nat).
-case_eq (Z.abs_nat z).
-intros K; absurd (z < 0)%Z; try easy.
-apply Zle_not_lt.
-rewrite <- Z.opp_involutive.
-rewrite <- (Z.abs_neq z).
-rewrite <- Zabs2Nat.id_abs, K.
-auto with zarith.
-auto with zarith.
-intros; auto with arith.
-unfold bij_NZ.
-case (even_odd_dec _); intros H2.
-contradict H2; intros H2.
-apply (not_even_and_odd (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.
-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.
-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.
+destruct (Z_lt_le_dec z 0) as [zlt0 | zge0].
+- (* z < 0 *)
+  unfold bij_NZ.
+  remember (Z.abs_nat z) as k eqn:def_k.
+  destruct k as [|k']; try lia.
+  replace (2 * (S k') - 1) with (2 * k' + 1) by lia.
+  assert (Odd_2k'1 : Nat.Odd (2 * k' + 1)) by now exists k'.
+  apply Nat.odd_spec in Odd_2k'1 as ->%negb_true_iff.
+  replace (Nat.div2 (2 * k' + 1 + 1)) with (k' + 1); try lia.
+  replace (2 * k' + 1 + 1) with (2 * (k' + 1)) by lia.
+  now rewrite Nat.div2_double.
+- (* z >= 0 *)
+  unfold bij_NZ.
+  assert (Even_2abs : Nat.Even (2 * Z.abs_nat z)) by now exists (Z.abs_nat z).
+  apply Nat.even_spec in Even_2abs as ->.
+  rewrite Nat.div2_double; lia.
 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.
-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.
-unfold Nat.double; auto with zarith.
-unfold bij_ZN.
-case (Z_lt_le_dec _ 0); intros H2.
-apply Nat2Z.inj.
-rewrite Nat2Z.inj_sub.
-rewrite Nat2Z.inj_mul.
-rewrite Nat2Z.inj_abs_nat.
-rewrite Z.abs_neq.
-2: auto with zarith.
-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.
-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.
-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.
-intros m Hm.
-contradict H2; apply Zlt_not_le.
-assert (0 < Nat.div2 (n+1))%nat.
-2: auto with zarith.
-apply div2_not_R0; auto with zarith.
+intros n; unfold bij_NZ, bij_ZN.
+destruct (Nat.even n) eqn:parity.
+- apply Nat.even_spec in parity as [k ->].
+  rewrite Nat.div2_double.
+  now destruct (Z_lt_le_dec (Z.of_nat k) 0) as [k_lt0 | k_geq0]; lia.
+- assert (n_odd : Nat.odd n = true) by now unfold Nat.odd; rewrite parity.
+  apply Nat.odd_spec in n_odd as [k ->].
+  replace (2 * k + 1 + 1) with (2 * (k + 1)) by lia.
+  rewrite Nat.div2_double.
+  now destruct (Z_lt_le_dec (-Z.of_nat (k + 1)) 0) as [k_lt0 | k_geq0]; lia.
 Qed.
-
 End Z_countable.
 
 
 Section N2_countable.
-
+Open Scope nat_scope.
 (* Use to_nat/of_nat from Arith.Cantor, appeared in Coq-8.14. *)
 
 Fixpoint bij_NN2_aux (n p : nat) : nat * nat :=
   match p with
-  | O => (0, 0)%nat
-  | S p' =>  match even_odd_dec n with
-    | left _ =>
+  | O => (0, 0)
+  | S p' =>  match Nat.even n with
+    | true =>
       let (u1, v1) := bij_NN2_aux (Nat.div2 n) p' in
       (S u1, v1)
-    | right _ => (0%nat, Nat.div2 n)
+    | false => (0, Nat.div2 n)
     end
   end.
 
+Lemma eq_couple {A B : Type} (a : A) (b : B) (z : A * B) :
+  (a, b) = z -> (a = fst z) /\ (b = snd z).
+Proof.
+  now intros <-.
+Qed.
+
 Lemma bij_NN2_aux_p :
   forall n p u v,
     (n <> 0)%nat -> (n <= p)%nat ->
@@ -165,94 +117,53 @@ apply (strong_induction (fun n =>
        forall (p u v:nat), (n <> 0)%nat -> (n <= p)%nat ->
          (u,v) =  bij_NN2_aux n p ->
         (n = Nat.pow 2 u * (S (2*v)))%nat)).
-intros n; case n.
-intros k p u v K; contradict K; auto with zarith.
+intros n; case n; try lia.
 clear n; intros n H p u v _ H2 H1.
 case_eq p.
 intros K; absurd (0 < p)%nat; auto with zarith.
 intros p' Hp'; generalize H1.
 rewrite Hp'; simpl.
-destruct (sumbool_rec _).
-(* even *)
-intros H3.
-assert (Hu: (u = S (fst (bij_NN2_aux (Nat.div2 (S n)) p')))%nat).
-apply trans_eq with (fst (u,v)); try easy.
-rewrite H3; simpl.
-destruct (bij_NN2_aux match n with
-                  | 0%nat => 0
-                  | S n' => S (Nat.div2 n')
-                  end p'); easy.
-assert (Hv: (v = snd (bij_NN2_aux (Nat.div2 (S n)) p'))%nat).
-apply trans_eq with (snd (u,v)); try easy.
-rewrite H3; simpl.
-destruct (bij_NN2_aux match n with
-                  | 0%nat => 0
-                  | S n' => S (Nat.div2 n')
-                  end p'); easy.
-assert (H4:Nat.div2 (S n) = (2 ^ (pred u) * S (2 * v))%nat).
-assert (Nat.div2 (S n) <> 0%nat).
-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 H with p'; try assumption.
-apply Div2.lt_div2; auto with zarith.
-assert (Nat.div2 (S n) < S n)%nat; auto with zarith.
-apply Div2.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.
-replace u with (S (pred u)) at 2.
-2: rewrite Hu; auto with zarith.
-rewrite Nat.pow_succ_r.
-2: auto with arith.
-unfold Nat.double; ring.
-(* *)
-intros H3.
-assert (Hu: (u = 0%nat)).
-apply trans_eq with (fst (u,v)); try easy.
-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.
-unfold Nat.double; simpl (2^0)%nat.
-ring.
+destruct n as [|n']; try now intros [= -> ->].
+destruct (Nat.even n') eqn:parity.
+- apply Nat.even_spec in parity as [k ->]; rewrite Nat.div2_double.
+  destruct (bij_NN2_aux (S k) p') as [u' v1] eqn:E.
+  intros [-> ->]%eq_couple; simpl.
+  assert (Sk_ltSSk : (S k) < S (S (2 *k))) by lia.
+  replace (S (S (k + (k + 0)))) with (2 * (S k)) by lia.
+  rewrite (H (S k) Sk_ltSSk p' u' v1); try easy; try lia.
+- apply negb_true_iff in parity.
+  replace (negb (Nat.even n')) with (Nat.odd n') by easy.
+  apply Nat.odd_spec in parity as [k ->].
+  rewrite Nat.add_1_r, Nat.div2_succ_double.
+  now intros [-> ->]%eq_couple; simpl; lia.
 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 ->
-  False).
-intros u v u' v' H1 H2.
-apply (not_even_and_odd (2^(u'-u)*(S (2*v'))))%nat.
-apply even_mult_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.
-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.
-apply Nat.mul_cancel_l with (Nat.pow 2 u).
-apply Nat.pow_nonzero; auto with arith.
-rewrite H2, Nat.mul_assoc.
-rewrite <- Nat.pow_add_r.
-f_equal; f_equal.
-auto with zarith.
+  (2 ^ u * (S (2*v)) = 2 ^ u' * (S (2*v')))%nat ->
+  False). {
+  intros u v u' v' H1 H2.
+  apply (Nat.Even_Odd_False (2^(u'-u)*(S (2*v'))))%nat.
+  - destruct (u' - u) eqn:u'u; try lia.
+    exists (2^n * S (2 * v')).
+    now rewrite Nat.mul_assoc, Nat.pow_succ_r'.
+  - replace (2 ^ (u' - u) * S (2 * v'))%nat with (S (2*v)).
+    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.
+    rewrite <- Nat.pow_add_r.
+    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 +196,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..3b8d08e0ee7039395cff71425fa70c8e9c4ad4aa 100644
--- a/Lebesgue/nat_compl.v
+++ b/Lebesgue/nat_compl.v
@@ -19,7 +19,6 @@ From Coq Require Import Arith Nat Lia.
 (*From Coq Require Import Streams.*)
 From Coquelicot Require Import Coquelicot.
 
-
 Section nat_compl.
 
 Lemma inhabited_nat : inhabited nat.
@@ -66,7 +65,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 +102,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 +121,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..40e0393a3ba41ddf93a0b62f1d5fa549bd910b00 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)))).
@@ -1399,7 +1397,7 @@ intros X; split; apply H1.
 apply open_and.
 apply open_fst.
 apply open_gt.
-apply open_fst with (A:=fun z => z < Q2R m1).
+apply (open_fst (fun z => z < Q2R m1)).
 apply open_lt.
 intros Y4; rewrite Y4.
 apply open_true.
@@ -1410,7 +1408,7 @@ intros X; split; apply H2.
 apply open_and.
 apply open_snd.
 apply open_gt.
-apply open_snd with (A:=fun z => z < Q2R m2).
+apply (open_snd (fun z => z < Q2R m2)).
 apply open_lt.
 intros Y4; rewrite Y4.
 apply open_true.
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).
 (* *)