From f30323e8f80f5c70e4df8eaa60fa257edb0d27e9 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cohen@crans.org>
Date: Thu, 4 Jun 2020 07:44:52 +0200
Subject: [PATCH] Adapting to new Order.max

---
 .github/workflows/nix.yml    |   2 +-
 .travis.yml                  |   4 +-
 config.nix                   |   4 +-
 theories/Rbar.v              |   8 +-
 theories/Rstruct.v           |  26 +++---
 theories/altreals/distr.v    |  15 ++-
 theories/altreals/realseq.v  |  10 +-
 theories/altreals/realsum.v  |  22 ++---
 theories/derive.v            |  12 +--
 theories/ereal.v             |  71 ++-------------
 theories/landau.v            |   4 +-
 theories/normedtype.v        | 172 +++++++++++++++++------------------
 theories/posnum.v            |  65 ++++++-------
 theories/prodnormedzmodule.v | 108 ++++++++++------------
 theories/sequences.v         |  10 +-
 theories/topology.v          |  12 +--
 16 files changed, 228 insertions(+), 317 deletions(-)

diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml
index ca2a0db653..74efacc7bd 100644
--- a/.github/workflows/nix.yml
+++ b/.github/workflows/nix.yml
@@ -16,5 +16,5 @@ jobs:
         name:  math-comp
         # Authentication token for Cachix, needed only for private cache access
         signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
-    - run: nix-build https://github.com/math-comp/math-comp-nix/archive/master.tar.gz --arg config '{mathcomp = "1.11.0+beta1"; mathcomp-analysis = "${{ steps.branch-short-name.outputs.branch }}";}' --argstr package mathcomp-analysis
+    - run: nix-build https://github.com/math-comp/math-comp-nix/archive/master.tar.gz --arg config '{mathcomp = "mathcomp-1.11.0"; mathcomp-analysis = "${{ steps.branch-short-name.outputs.branch }}";}' --argstr package mathcomp-analysis
     # - run: export CACHIX_SIGNING_KEY=${{ secrets.CACHIX_SIGNING_KEY }} cachix push math-comp result
diff --git a/.travis.yml b/.travis.yml
index 2cb49ebfa6..e750a9d7dd 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -21,8 +21,8 @@ install:
 - docker pull ${DOCKERIMAGE}
 - docker tag  ${DOCKERIMAGE} ci:current
 - docker run  --env=OPAMYES --init -id --name=CI -v ${TRAVIS_BUILD_DIR}:/home/coq/${CONTRIB} -w /home/coq/${CONTRIB} ci:current
-- docker exec CI /bin/bash --login -c "cd ..; curl -LO https://github.com/math-comp/finmap/archive/1.5.0.tar.gz; tar -xvzf 1.5.0.tar.gz; cd finmap-1.5.0/; opam pin add -y -n coq-mathcomp-finmap.1.5.0 .; opam install coq-mathcomp-finmap.1.5.0; cd /home/coq/${CONTRIB}"
-- docker exec CI /bin/bash --login -c "opam pin add -y -n coq-mathcomp-${CONTRIB} ."
+- docker exec CI /bin/bash --login -c "opam update -y"
+- docker exec CI /bin/bash --login -c "opam pin add -n -y -k path coq-mathcomp-${CONTRIB}.dev ."
 - docker exec CI /bin/bash --login -c "opam install --deps-only coq-mathcomp-${CONTRIB}"
 
 script:
diff --git a/config.nix b/config.nix
index 7b5a3aeb5b..06b6cb7b82 100644
--- a/config.nix
+++ b/config.nix
@@ -1,5 +1,5 @@
 {
   coq = "8.10";
-  mathcomp = "1.11.0+beta1";
-  mathcomp-real-closed = "1.1.0";
+  mathcomp = "mathcomp-1.11.0";
+  mathcomp-real-closed = "1.1.1";
 }
diff --git a/theories/Rbar.v b/theories/Rbar.v
index b23357a17e..b76bc45b65 100644
--- a/theories/Rbar.v
+++ b/theories/Rbar.v
@@ -525,8 +525,8 @@ move=> [:wlog]; case: a b => [a||] [b||] //= ltax ltxb.
 - move: a b ltax ltxb; abstract: wlog. (*BUG*)
   move=> {a b} a b ltxa ltxb.
   have m_gt0 : Num.min ((x - a) / 2) ((b - x) / 2) > 0.
-    by rewrite ltxI !divr_gt0 ?subr_gt0.
-  exists (PosNum m_gt0) => y //=; rewrite ltxI !ltr_distl.
+    by rewrite lt_minr !divr_gt0 ?subr_gt0.
+  exists (PosNum m_gt0) => y //=; rewrite lt_minr !ltr_distl.
   move=> /andP[/andP[ay _] /andP[_ yb]].
   rewrite (lt_trans _ ay) ?(lt_trans yb) //=.
     by rewrite -subr_gt0 opprD addrA {1}[b - x]splitr addrK divr_gt0 ?subr_gt0.
@@ -539,10 +539,10 @@ move=> [:wlog]; case: a b => [a||] [b||] //= ltax ltxb.
 Qed.
 
 Lemma Rbar_min_comm (x y : Rbar) : Rbar_min x y = Rbar_min y x.
-Proof. by case: x y => [x||] [y||] //=; rewrite meetC. Qed.
+Proof. by case: x y => [x||] [y||] //=; rewrite minC. Qed.
 
 Lemma Rbar_min_r (x y : Rbar) : Rbar_le (Rbar_min x y) y.
-Proof. by case: x y => [x||] [y||] //=; rewrite leIx lexx orbT. Qed.
+Proof. by case: x y => [x||] [y||] //=; rewrite le_minl lexx orbT. Qed.
 
 Lemma Rbar_min_l (x y : Rbar) : Rbar_le (Rbar_min x y) x.
 Proof. by rewrite Rbar_min_comm Rbar_min_r. Qed.
diff --git a/theories/Rstruct.v b/theories/Rstruct.v
index 24936494b9..d24e909ee0 100644
--- a/theories/Rstruct.v
+++ b/theories/Rstruct.v
@@ -482,15 +482,15 @@ Proof. by elim: n => [ | n In] //=; rewrite exprS In RmultE. Qed.
 
 Lemma RmaxE x y : Rmax x y = Num.max x y.
 Proof.
-case: (lerP x y) => H; first by rewrite join_r // Rmax_right //; apply: RlebP.
-by rewrite join_l ?ltW // Rmax_left //;  apply/RlebP; move/ltW : H.
+case: (lerP x y) => H; first by rewrite Rmax_right //; apply: RlebP.
+by rewrite ?ltW // Rmax_left //;  apply/RlebP; move/ltW : H.
 Qed.
 
 (* useful? *)
 Lemma RminE x y : Rmin x y = Num.min x y.
 Proof.
-case: (lerP x y) => H; first by rewrite meet_l // Rmin_left //; apply: RlebP.
-by rewrite meet_r ?ltW // Rmin_right //;  apply/RlebP; move/ltW : H.
+case: (lerP x y) => H; first by rewrite Rmin_left //; apply: RlebP.
+by rewrite ?ltW // Rmin_right //;  apply/RlebP; move/ltW : H.
 Qed.
 
 Section bigmaxr.
@@ -503,14 +503,14 @@ Lemma bigmaxr_nil (x0 : R) : bigmaxr x0 [::] = x0.
 Proof. by rewrite /bigmaxr /= big_nil. Qed.
 
 Lemma bigmaxr_un (x0 x : R) : bigmaxr x0 [:: x] = x.
-Proof. by rewrite /bigmaxr /= big_cons big_nil joinxx. Qed.
+Proof. by rewrite /bigmaxr /= big_cons big_nil maxxx. Qed.
 
 (* previous definition *)
 Lemma bigmaxrE (r : R) s : bigmaxr r s = foldr Num.max (head r s) (behead s).
 Proof.
 rewrite (_ : bigmaxr _ _ = if s isn't h :: t then r else \big[Num.max/h]_(i <- s) i).
   case: s => // ? t; rewrite big_cons /bigmaxr.
-  by elim: t => //= [|? ? <-]; [rewrite big_nil joinxx | rewrite big_cons joinCA].
+  by elim: t => //= [|? ? <-]; [rewrite big_nil maxxx | rewrite big_cons maxCA].
 by case: s => //=; rewrite /bigmaxr big_nil.
 Qed.
 
@@ -518,8 +518,8 @@ Lemma bigrmax_dflt (x y : R) s : Num.max x (\big[Num.max/x]_(j <- y :: s) j) =
   Num.max x (\big[Num.max/y]_(i <- y :: s) i).
 Proof.
 elim: s => /= [|h t IH] in x y *.
-by rewrite !big_cons !big_nil joinxx joinCA joinxx joinC.
-by rewrite big_cons joinCA IH joinCA [in RHS]big_cons IH.
+by rewrite !big_cons !big_nil maxxx maxCA maxxx maxC.
+by rewrite big_cons maxCA IH maxCA [in RHS]big_cons IH.
 Qed.
 
 Lemma bigmaxr_cons (x0 x y : R) lr :
@@ -530,9 +530,9 @@ Lemma bigmaxr_ler (x0 : R) s i :
   (i < size s)%N -> (nth x0 s i) <= (bigmaxr x0 s).
 Proof.
 rewrite /bigmaxr; elim: s i => // h t IH [_|i] /=.
-  by rewrite big_cons /= lexU lexx.
+  by rewrite big_cons /= le_maxr lexx.
 rewrite ltnS => ti; case: t => [|h' t] // in IH ti *.
-by rewrite big_cons bigrmax_dflt lexU orbC IH.
+by rewrite big_cons bigrmax_dflt le_maxr orbC IH.
 Qed.
 
 (* Compatibilité avec l'addition *)
@@ -547,10 +547,10 @@ Qed.
 Lemma bigmaxr_mem (x0 : R) lr : (0 < size lr)%N -> bigmaxr x0 lr \in lr.
 Proof.
 rewrite /bigmaxr; case: lr => // h t _.
-elim: t => //= [|h' t IH] in h *; first by rewrite big_cons big_nil inE joinxx.
+elim: t => //= [|h' t IH] in h *; first by rewrite big_cons big_nil inE maxxx.
 rewrite big_cons bigrmax_dflt inE eq_le; case: lerP => /=.
-- by rewrite lexU lexx.
-- by rewrite ltxU ltxx => ?; rewrite join_r ?IH // ltW.
+- by rewrite le_maxr lexx.
+- by rewrite lt_maxr ltxx => ?; rewrite max_r ?IH // ltW.
 Qed.
 
 (* TODO: bigmaxr_morph? *)
diff --git a/theories/altreals/distr.v b/theories/altreals/distr.v
index b480132ba3..e475eb5f28 100644
--- a/theories/altreals/distr.v
+++ b/theories/altreals/distr.v
@@ -79,18 +79,15 @@ Definition clamp (x : R) :=
   Num.max (Num.min x 1) 0.
 
 Lemma ge0_clamp x : 0 <= clamp x.
-Proof. by rewrite lexU lexx orbT. Qed.
+Proof. by rewrite le_maxr lexx orbT. Qed.
 
 Lemma le1_clamp x : clamp x <= 1.
-Proof. by rewrite leUx leIx lexx ler01 orbT. Qed.
+Proof. by rewrite le_maxl le_minl lexx ler01 orbT. Qed.
 
 Definition cp01_clamp := (ge0_clamp, le1_clamp).
 
 Lemma clamp_in01 x : 0 <= x <= 1 -> clamp x = x.
-Proof.
-case/andP=> ge0_x le1_x; rewrite /clamp (elimT join_idPr).
-  by rewrite lexI ge0_x ler01. by rewrite (elimT meet_idPl).
-Qed.
+Proof. by case/andP=> ge0_x le1_x; rewrite /clamp min_l ?max_l. Qed.
 
 Lemma clamp_id x : clamp (clamp x) = clamp x.
 Proof. by rewrite clamp_in01 // !cp01_clamp. Qed.
@@ -1144,14 +1141,14 @@ Lemma has_esp_bounded f mu :
   (exists M, forall x, `|f x| < M) -> \E?_[mu] f.
 Proof.                          (* TO BE REMOVED *)
 case=> M ltM; rewrite /has_esp; apply/summable_seqP.
-exists (Num.max M 0); first by rewrite lexU lexx orbT.
+exists (Num.max M 0); first by rewrite le_maxr lexx orbT.
 move=> J uqJ; apply/(@le_trans _ _ (\sum_(j <- J) M * mu j)).
   apply/ler_sum=> j _; rewrite normrM [X in _*X]ger0_norm //.
   by apply/ler_wpmul2r=> //; apply/ltW.
 case: (ltrP M 0) => [lt0_M|ge0_M].
-  rewrite (elimT join_idPl) ?(ltW lt0_M) // -mulr_sumr.
+  rewrite ?(ltW lt0_M) // -mulr_sumr.
   by rewrite nmulr_rle0 //; apply/sumr_ge0.
-by rewrite (elimT join_idPr) // -mulr_sumr ler_pimulr // -pr_mem ?le1_pr.
+by rewrite -mulr_sumr ler_pimulr // -pr_mem ?le1_pr.
 Qed.
 
 Lemma bounded_has_exp mu F :
diff --git a/theories/altreals/realseq.v b/theories/altreals/realseq.v
index 393c996728..7632e65ace 100644
--- a/theories/altreals/realseq.v
+++ b/theories/altreals/realseq.v
@@ -215,20 +215,20 @@ Lemma ncvg_nbounded u x : ncvg u x%:E -> nbounded u.
 Proof.                   (* FIXME: factor out `sup` of a finite set *)
 case/(_ (B x 1)) => K cu; pose S := [seq `|u n| | n <- iota 0 K].
 pose M : R := sup [set x : R | x \in S]; pose e := Num.max (`|x| + 1) (M + 1).
-apply/asboolP/nboundedP; exists e => [|n]; first by rewrite ltxU ltr_paddl.
+apply/asboolP/nboundedP; exists e => [|n]; first by rewrite lt_maxr ltr_paddl.
 case: (ltnP n K); last first.
   move/cu; rewrite inE eclamp_id ?ltr01 // => ltunBx1.
-  rewrite ltxU; apply/orP; left; rewrite -[u n](addrK x) addrAC.
+  rewrite lt_maxr; apply/orP; left; rewrite -[u n](addrK x) addrAC.
   by apply/(le_lt_trans (ler_norm_add _ _)); rewrite addrC ltr_add2l.
 move=> lt_nK; have: `|u n| \in S; first by apply/map_f; rewrite mem_iota.
-move=> un_S; rewrite ltxU; apply/orP; right.
+move=> un_S; rewrite lt_maxr; apply/orP; right.
 case E: {+}K lt_nK => [|k] // lt_nSk; apply/ltr_spaddr; first apply/ltr01.
 suff : has_sup (fun x : R => x \in S) by move/sup_upper_bound/ubP => ->.
 split; first by exists `|u 0%N|; rewrite /S E inE eqxx.
 elim: {+}S => [|v s [ux /ubP hux]]; first by exists 0; apply/ubP.
 exists (Num.max v ux); apply/ubP=> y; rewrite inE => /orP[/eqP->|].
-  by rewrite lexU lexx.
-by move/hux=> le_yux; rewrite lexU le_yux orbT.
+  by rewrite le_maxr lexx.
+by move/hux=> le_yux; rewrite le_maxr le_yux orbT.
 Qed.
 
 Lemma nboundedC c : nbounded c%:S.
diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v
index fceeb7afe9..13063eaa6e 100644
--- a/theories/altreals/realsum.v
+++ b/theories/altreals/realsum.v
@@ -54,10 +54,10 @@ Lemma eq_fneg f g : f =1 g -> fneg f =1 fneg g.
 Proof. by move=> eq_fg x; rewrite /fneg eq_fg. Qed.
 
 Lemma fpos0 x : fpos (fun _ : T => 0) x = 0 :> R.
-Proof. by rewrite /fpos joinxx normr0. Qed.
+Proof. by rewrite /fpos maxxx normr0. Qed.
 
 Lemma fneg0 x : fneg (fun _ : T => 0) x = 0 :> R.
-Proof. by rewrite /fneg meetxx normr0. Qed.
+Proof. by rewrite /fneg minxx normr0. Qed.
 
 Lemma fnegN f : fneg (\- f) =1 fpos f.
 Proof. by move=> x; rewrite /fpos /fneg -{1}oppr0 -oppr_max normrN. Qed.
@@ -92,10 +92,10 @@ by apply/eq_fpos=> y; rewrite mulrN.
 Qed.
 
 Lemma fneg_ge0 f x : (forall x, 0 <= f x) -> fneg f x = 0.
-Proof. by move=> ?; rewrite /fneg (elimT meet_idPl) ?normr0. Qed.
+Proof. by move=> ?; rewrite /fneg min_l ?normr0. Qed.
 
 Lemma fpos_ge0 f x : (forall x, 0 <= f x ) -> fpos f x = f x.
-Proof. by move=> ?; rewrite /fpos (elimT join_idPl) ?ger0_norm. Qed.
+Proof. by move=> ?; rewrite /fpos max_r ?ger0_norm. Qed.
 
 Lemma ge0_fpos f x : 0 <= fpos f x.
 Proof. by apply/normr_ge0. Qed.
@@ -105,19 +105,19 @@ Proof. by apply/normr_ge0. Qed.
 
 Lemma le_fpos_norm f x : fpos f x <= `|f x|.
 Proof.
-rewrite /fpos ger0_norm ?(lexU, lexx) //.
-by rewrite leUx normr_ge0 ler_norm.
+rewrite /fpos ger0_norm ?(le_maxr, lexx) //.
+by rewrite le_maxl normr_ge0 ler_norm.
 Qed.
 
 Lemma le_fpos f1 f2 : f1 <=1 f2 -> fpos f1 <=1 fpos f2.
 Proof.
-move=> le_f x; rewrite /fpos !ger0_norm ?lexU ?lexx //.
-by rewrite leUx lexx /=; case: ltP => //=; rewrite le_f.
+move=> le_f x; rewrite /fpos !ger0_norm ?le_maxr ?lexx //.
+by rewrite le_maxl lexx /=; case: ltP => //=; rewrite le_f.
 Qed.
 
 Lemma fposBfneg f x : fpos f x - fneg f x = f x.
 Proof.
-rewrite /fpos /fneg joinC.
+rewrite /fpos /fneg maxC.
 case: (leP (f x) 0); rewrite normr0 (subr0, sub0r) => ?.
   by rewrite ler0_norm ?opprK.
 by rewrite gtr0_norm.
@@ -1177,10 +1177,10 @@ Proof.
 move=> eqr domS; rewrite /sum !(psum_finseq eqr).
 + move=> x; rewrite !inE => xPS; apply/domS; rewrite !inE.
   move: xPS; rewrite /fpos normr_eq0.
-  by apply: contra => /eqP ->; rewrite joinxx.
+  by apply: contra => /eqP ->; rewrite maxxx.
 + move=> x; rewrite !inE => xPS; apply/domS; rewrite !inE.
   move: xPS; rewrite /fneg normr_eq0.
-  by apply: contra => /eqP ->; rewrite meetxx.
+  by apply: contra => /eqP ->; rewrite minxx.
 rewrite -sumrB; apply/eq_bigr=> i _.
 by rewrite !ger0_norm ?(ge0_fpos, ge0_fneg) ?fposBfneg.
 Qed.
diff --git a/theories/derive.v b/theories/derive.v
index a930bff999..82699e655c 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -768,11 +768,7 @@ have -> : (ku^-1 *: u, kv^-1 *: v) =
   rewrite mulrC -[_ *: u]scalerA [X in X *: v]mulrC -[_ *: v]scalerA.
   by rewrite invf_div.
 rewrite normmZ ger0_norm // -mulrA gtr_pmulr // ltr_pdivr_mull // mulr1.
-rewrite prod_normE /= (_ : _%:nng = 1%:nng); last first.
-  by apply/val_inj => /=; rewrite normmZ normrV ?unitfE ?gt_eqF // normr_id mulVf ?gt_eqF.
-rewrite (_ : _%:nng = 1%:nng); last first.
-  by apply/val_inj => /=; rewrite normmZ normrV ?unitfE ?gt_eqF // normr_id mulVf ?gt_eqF.
-by rewrite joinxx /= ltr1n.
+by rewrite prod_normE/= !normmZ !normfV !normr_id !mulVf ?gt_eqF// maxxx ltr1n.
 Qed.
 
 Lemma bilinear_eqo (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) :
@@ -780,9 +776,9 @@ Lemma bilinear_eqo (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) :
 Proof.
 move=> fc; have [_ /posnumP[k] fschwarz] := bilinear_schwarz fc.
 apply/eqoP=> _ /posnumP[e]; near=> x; rewrite (le_trans (fschwarz _ _))//.
-rewrite ler_pmul ?pmulr_rge0 //; last by rewrite nng_lexU /= lexx orbT.
+rewrite ler_pmul ?pmulr_rge0 //; last by rewrite nng_le_maxr /= lexx orbT.
 rewrite -ler_pdivl_mull //.
-suff : `|x| <= k%:num ^-1 * e%:num by apply: le_trans; rewrite nng_lexU /= lexx.
+suff : `|x| <= k%:num ^-1 * e%:num by apply: le_trans; rewrite nng_le_maxr /= lexx.
 near: x; rewrite !near_simpl; apply/locally_le_locally_norm.
 by exists (k%:num ^-1 * e%:num) => // ? /=; rewrite distrC subr0 => /ltW.
 Grab Existential Variables. all: end_near. Qed.
@@ -846,7 +842,7 @@ Lemma eqo_pair (U V' W' : normedModType R) (F : filter_on U)
   (f : U -> V') (g : U -> W') :
   (fun t => ([o_F id of f] t, [o_F id of g] t)) =o_F id.
 Proof.
-apply/eqoP => _/posnumP[e]; near=> x; rewrite nng_leUx /=.
+apply/eqoP => _/posnumP[e]; near=> x; rewrite nng_le_maxl /=.
 by apply/andP; split; near: x; apply: littleoP.
 Grab Existential Variables. all: end_near. Qed.
 
diff --git a/theories/ereal.v b/theories/ereal.v
index c624a0316d..6a1bb1b5a7 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -156,6 +156,9 @@ Definition ereal_porderMixin :=
 Canonical ereal_porderType :=
   POrderType ereal_display {ereal R} ereal_porderMixin.
 
+Lemma leEereal x y : (x <= y)%O = le_ereal x y. Proof. by []. Qed.
+Lemma ltEereal x y : (x < y)%O = lt_ereal x y. Proof. by []. Qed.
+
 End ERealOrder.
 
 Notation lee := (@Order.le ereal_display _) (only parsing).
@@ -179,16 +182,16 @@ Proof. by []. Qed.
 Lemma lte_fin (R : numDomainType) (x y : R) : (x%:E < y%:E)%E = (x < y)%O.
 Proof. by []. Qed.
 
-Lemma lte_pinfty (R : realDomainType) (x : R) : (x%:E < +oo).
+Lemma lte_pinfty (R : realDomainType) (x : R) : x%:E < +oo.
 Proof. exact: num_real. Qed.
 
-Lemma lee_pinfty (R : realDomainType) (x : {ereal R}) : (x <= +oo).
+Lemma lee_pinfty (R : realDomainType) (x : {ereal R}) : x <= +oo.
 Proof. case: x => //= r; exact: num_real. Qed.
 
 Lemma lte_ninfty (R : realDomainType) (x : R) : (-oo < x%:E).
 Proof. exact: num_real. Qed.
 
-Lemma lee_ninfty (R : realDomainType) (x : {ereal R}) : (-oo <= x).
+Lemma lee_ninfty (R : realDomainType) (x : {ereal R}) : -oo <= x.
 Proof. case: x => //= r; exact: num_real. Qed.
 
 Lemma lee_ninfty_eq (R : numDomainType) (x : {ereal R}) : (x <= -oo)%E = (x == -oo%E).
@@ -201,67 +204,13 @@ Section ERealOrder_realDomainType.
 Context {R : realDomainType}.
 Implicit Types (x y : {ereal R}).
 
-Definition min_ereal x1 x2 :=
-  match x1, x2 with
-  | -oo, _ | _, -oo => -oo
-  | +oo, x | x, +oo => x
-
-  | x1%:E, x2%:E => (Num.Def.minr x1 x2)%:E
-  end.
-
-Definition max_ereal x1 x2 :=
-  match x1, x2 with
-  | -oo, x | x, -oo => x
-  | +oo, _ | _, +oo => +oo
-
-  | x1%:E, x2%:E => (Num.Def.maxr x1 x2)%:E
-  end.
-
-Lemma min_erealC : commutative min_ereal.
-Proof. by case=> [?||][?||] //=; rewrite meetC. Qed.
-
-Lemma max_erealC : commutative max_ereal.
-Proof. by case=> [?||][?||] //=; rewrite joinC. Qed.
-
-Lemma min_erealA : associative min_ereal.
-Proof. by case=> [?||][?||][?||] //=; rewrite meetA. Qed.
-
-Lemma max_erealA : associative max_ereal.
-Proof. by case=> [?||][?||][?||] //=; rewrite joinA. Qed.
-
-Lemma joinKI_ereal y x : min_ereal x (max_ereal x y) = x.
-Proof. by case: x y => [?||][?||] //=; rewrite (joinKI, meetxx). Qed.
-
-Lemma meetKU_ereal y x : max_ereal x (min_ereal x y) = x.
-Proof. by case: x y => [?||][?||] //=; rewrite (meetKU, joinxx). Qed.
-
-Lemma leEmeet_ereal x y : (x <= y)%E = (min_ereal x y == x).
-Proof.
-case: x y => [x||][y||] //=; rewrite ?eqxx ?lee_pinfty ?lee_ninfty //.
-exact: leEmeet.
-Qed.
-
-Lemma meetUl_ereal : left_distributive min_ereal max_ereal.
+Lemma le_total_ereal : totalPOrderMixin [porderType of {ereal R}].
 Proof.
-by case=> [?||][?||][?||] //=; rewrite ?(meetUl, meetUK, meetKUC, joinxx).
+by move=> [?||][?||]//=; rewrite (ltEereal, leEereal)/= ?num_real ?le_total.
 Qed.
 
-Lemma minE_ereal x y : min_ereal x y = if le_ereal x y then x else y.
-Proof. by case: x y => [?||][?||] //=; rewrite ?num_real //; case: leP. Qed.
-
-Lemma maxE_ereal x y : max_ereal x y = if le_ereal y x then x else y.
-Proof. by case: x y => [?||][?||] //=; rewrite ?num_real //; case: ltP. Qed.
-
-Lemma le_total_ereal : total (@le_ereal R).
-Proof. by case=> [?||][?||] //=; rewrite ?num_real //; exact: le_total. Qed.
-
-Definition ereal_latticeMixin :=
-  LatticeMixin min_erealC max_erealC min_erealA max_erealA
-                    joinKI_ereal meetKU_ereal leEmeet_ereal.
-Canonical ereal_latticeType := LatticeType {ereal R} ereal_latticeMixin.
-Definition ereal_distrLatticeMixin := DistrLatticeMixin meetUl_ereal.
-Canonical ereal_distrLatticeType :=
-  DistrLatticeType {ereal R} ereal_distrLatticeMixin.
+Canonical ereal_latticeType := LatticeType {ereal R} le_total_ereal.
+Canonical ereal_distrLatticeType :=  DistrLatticeType {ereal R} le_total_ereal.
 Canonical ereal_orderType := OrderType {ereal R} le_total_ereal.
 
 End ERealOrder_realDomainType.
diff --git a/theories/landau.v b/theories/landau.v
index b354fedbff..d7671579eb 100644
--- a/theories/landau.v
+++ b/theories/landau.v
@@ -469,10 +469,10 @@ split=> [[k k0 fOg] | [k [kreal fOg]]].
   exists k; rewrite realE (ltW k0) /=; split=> // l ltkl; move: fOg.
   by apply: filter_app; near=> x => /le_trans; apply; rewrite ler_wpmul2r // ltW.
 exists (Num.max 1%:nng `|k + 1|%:nng)%:nngnum.
-  by rewrite -nng_lt /= ltxU /= nng_lt ltr01.
+  by rewrite nng_lt /= lt_maxr /= -nng_lt ltr01.
 apply: fOg; rewrite (@lt_le_trans _ _ `|k + 1|) //.
 by rewrite (@lt_le_trans _ _ (k + 1)) ?ltr_addl // real_ler_norm ?(realD,real1).
-by rewrite -nng_le lexU orbC lexx.
+by rewrite nng_le le_maxr orbC lexx.
 Unshelve. end_near. Qed.
 
 Structure bigO_type (F : set (set T)) (g : T -> W) := BigO {
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 485c19eb81..918addfde9 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -615,7 +615,7 @@ case=> [x||].
     exists (Num.max (PosNum MP0) (PosNum MQ0))%:num.
     rewrite realE /= posnum_ge0 /=; split => //.
     case=> [r| |//].
-    * rewrite lte_fin pos_ltUx /= => /andP[MPx MQx]; split.
+    * rewrite lte_fin/= posnum_max pos_lt_maxl /= => /andP[MPx MQx]; split.
       by apply/gtMP; rewrite lte_fin (le_lt_trans _ MPx) // real_ler_normr // lexx.
       by apply/gtMQ; rewrite lte_fin (le_lt_trans _ MQx) // real_ler_normr // lexx.
     * by move=> _; split; [apply/gtMP | apply/gtMQ].
@@ -643,7 +643,7 @@ case=> [x||].
       exists (- (Num.max (PosNum MP0) (PosNum MQ0))%:num).
       rewrite realN realE /= posnum_ge0 /=; split => //.
       case=> [r|//|].
-      - rewrite lte_fin ltr_oppr pos_ltUx => /andP[].
+      - rewrite lte_fin ltr_oppr posnum_max pos_lt_maxl => /andP[].
         rewrite ltr_oppr => MPx; rewrite ltr_oppr => MQx; split.
           apply/ltMP; rewrite lte_fin (lt_le_trans MPx) //= ler_oppl -normrN.
           by rewrite real_ler_normr ?realN // lexx.
@@ -765,7 +765,7 @@ split=> /= [|P Q [MP [MPr gtMP]] [MQ [MQr gtMQ]] |P Q sPQ [M [Mr gtM]]].
   have {}MQ0 : 0 < `|MQ| by rewrite normr_gt0.
   exists (Num.max (PosNum MP0) (PosNum MQ0))%:num.
   rewrite realE /= posnum_ge0 /=; split => // x.
-  rewrite pos_ltUx /= => /andP[MPx MQx]; split.
+  rewrite posnum_max pos_lt_maxl /= => /andP[MPx MQx]; split.
   by apply/gtMP; rewrite (le_lt_trans _ MPx) // real_ler_normr // lexx.
   by apply/gtMQ; rewrite (le_lt_trans _ MQx) // real_ler_normr // lexx.
 - by exists M; split => // ? /gtM /sPQ.
@@ -796,7 +796,7 @@ apply Build_ProperFilter.
     have {}MQ0 : 0 < `|MQ| by rewrite normr_gt0.
     exists (- (Num.max (PosNum MP0) (PosNum MQ0))%:num).
     rewrite realN realE /= posnum_ge0 /=; split => // x.
-    rewrite ltr_oppr pos_ltUx => /andP[].
+    rewrite ltr_oppr posnum_max pos_lt_maxl => /andP[].
     rewrite ltr_oppr => MPx; rewrite ltr_oppr => MQx; split.
       apply/ltMP; rewrite (lt_le_trans MPx) //= ler_oppl -normrN.
       by rewrite real_ler_normr ?realN // lexx.
@@ -829,7 +829,7 @@ case=> [x||]; first exact: Proper_locally'_numFieldType.
     have {}MQ0 : 0 < `|MQ| by rewrite normr_gt0.
     exists (Num.max (PosNum MP0) (PosNum MQ0))%:num.
     rewrite realE /= posnum_ge0 /=; split => // x.
-    rewrite pos_ltUx /= => /andP[MPx MQx]; split.
+    rewrite pos_lt_maxl /= => /andP[MPx MQx]; split.
     by apply/gtMP; rewrite (le_lt_trans _ MPx) // real_ler_normr // lexx.
     by apply/gtMQ; rewrite (le_lt_trans _ MQx) // real_ler_normr // lexx.
   + by exists M; split => // ? /gtM /sPQ.
@@ -855,7 +855,7 @@ case=> [x||]; first exact: Proper_locally'_numFieldType.
       have {}MQ0 : 0 < `|MQ| by rewrite normr_gt0.
       exists (- (Num.max (PosNum MP0) (PosNum MQ0))%:num).
       rewrite realN realE /= posnum_ge0 /=; split => // x.
-      rewrite ltr_oppr pos_ltUx => /andP[].
+      rewrite ltr_oppr pos_lt_maxl => /andP[].
       rewrite ltr_oppr => MPx; rewrite ltr_oppr => MQx; split.
         apply/ltMP; rewrite (lt_le_trans MPx) //= ler_oppl -normrN.
         by rewrite real_ler_normr ?realN // lexx.
@@ -1427,7 +1427,7 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1].
     pose e' : R := minr (r - real_of_er (expand (contract r%:E - e%:num)))
                         (real_of_er (expand (contract r%:E + e%:num)) - r).
     have e'0 : 0 < e'.
-      rewrite /e' ltxI; apply/andP; split.
+      rewrite /e' lt_minr; apply/andP; split.
         rewrite subr_gt0 -lte_fin -[in X in (_ < X)%E](contractK r%:E).
         rewrite real_of_er_expand // lt_expand// ?inE ?contract_le1 ?ltW//.
         by rewrite ltr_subl_addl ltr_addr.
@@ -1442,10 +1442,10 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1].
       rewrite ltr0_norm ?subr_lt0// opprB in re'r'.
       rewrite ltr0_norm ?subr_lt0 ?lt_contract ?lte_fin//.
       rewrite opprB; move: re'r'.
-      rewrite /e' ltxI => /andP[_].
+      rewrite /e' lt_minr => /andP[_].
       rewrite -ltr_subl_addr opprK subrK -lte_fin real_of_er_expand //.
       by move=> r'e'r; rewrite ltr_subl_addl -lt_expandRL ?inE ?ltW.
-    move: re'r'; rewrite ltxI => /andP[].
+    move: re'r'; rewrite lt_minr => /andP[].
     rewrite gtr0_norm ?subr_gt0 // -ltr_subl_addl addrAC subrr add0r ltr_oppl.
     rewrite opprK -lte_fin real_of_er_expand // => r'e'r _.
     rewrite gtr0_norm ?subr_gt0 ?lt_contract ?lte_fin//.
@@ -1487,7 +1487,7 @@ rewrite predeq2E => x A; split.
   + pose e' : R := minr (contract r%:E - contract (r%:E - e%:num%:E))
                         (contract (r%:E + e%:num%:E) - contract r%:E).
     exists e'.
-      rewrite /e' ltxI; apply/andP; split.
+      rewrite /e' lt_minr; apply/andP; split.
         by rewrite subr_gt0 lt_contract lte_fin ltr_subl_addr ltr_addl.
       by rewrite subr_gt0 lt_contract lte_fin ltr_addl.
     case=> [r' re'r'| |].
@@ -1497,7 +1497,7 @@ rewrite predeq2E => x A; split.
         rewrite /ball_ real_ltr_norml // ?num_real //.
         rewrite ger0_norm ?subr_ge0// in re'r'.
         have H1 : contract (r%:E - e%:num%:E) < contract r'%:E.
-          move: re'r'; rewrite /e' ltxI => /andP[Hr'1 Hr'2].
+          move: re'r'; rewrite /e' lt_minr => /andP[Hr'1 Hr'2].
           rewrite /e' ltr_subr_addl addrC -ltr_subr_addl in Hr'1.
           by rewrite (lt_le_trans Hr'1) // opprB addrCA subrr addr0.
         have := H1;  rewrite -lt_expandRL ?inE ?contract_le1 //.
@@ -1514,12 +1514,12 @@ rewrite predeq2E => x A; split.
       rewrite ltr_oppl opprB.
       rewrite /e' in re'r'.
       have H2 : contract r'%:E < contract (r%:E + e%:num%:E).
-        move: re'r'; rewrite ltxI => /andP[Hr'1 Hr'2].
+        move: re'r'; rewrite lt_minr => /andP[Hr'1 Hr'2].
         by rewrite ltr_subl_addr subrK in Hr'2.
       rewrite ltr_subl_addr -lte_fin -(contractK (_ + r)%:E).
       by rewrite addrC -(contractK r'%:E) // lt_expand ?inE ?contract_le1.
     * rewrite /ereal_ball [contract +oo]/=.
-      rewrite ltxI => /andP[re'1 re'2].
+      rewrite lt_minr => /andP[re'1 re'2].
       have [cr0|cr0] := lerP 0 (contract r%:E).
         move: re'2; rewrite ler0_norm; last first.
           by rewrite subr_le0; case/ler_normlP : (contract_le1 r%:E).
@@ -1534,7 +1534,7 @@ rewrite predeq2E => x A; split.
       move: h; apply/negP; rewrite -leNgt.
       by case/ler_normlP : (contract_le1 (r%:E + e%:num%:E)).
     * rewrite /ereal_ball [contract -oo]/=; rewrite opprK.
-      rewrite ltxI => /andP[re'1 _].
+      rewrite lt_minr => /andP[re'1 _].
       move: re'1.
       rewrite ger0_norm; last first.
         rewrite addrC -ler_subl_addl add0r.
@@ -2127,24 +2127,24 @@ Lemma bigmaxr_mkcond I r (P : pred I) (F : I -> {nonneg R}) x :
      \big[maxr/x]_(i <- r) (if P i then F i else x).
 Proof.
 rewrite unlock; elim: r x => //= i r ihr x.
-case P; rewrite ihr // join_r //; elim: r {ihr} => //= j r ihr.
-by rewrite lexU ihr orbT.
+case P; rewrite ihr // max_r //; elim: r {ihr} => //= j r ihr.
+by rewrite le_maxr ihr orbT.
 Qed.
 
 Lemma bigmaxr_split I r (P : pred I) (F1 F2 : I -> {nonneg R}) x :
   \big[maxr/x]_(i <- r | P i) (maxr (F1 i) (F2 i)) =
   maxr (\big[maxr/x]_(i <- r | P i) F1 i) (\big[maxr/x]_(i <- r | P i) F2 i).
 Proof.
-elim/big_rec3: _ => [|i y z _ _ ->]; rewrite ?joinxx //.
-by rewrite joinCA -!joinA joinCA.
+elim/big_rec3: _ => [|i y z _ _ ->]; rewrite ?maxxx //.
+by rewrite maxCA -!maxA maxCA.
 Qed.
 
 Lemma bigmaxr_idl I r (P : pred I) (F : I -> {nonneg R}) x :
   \big[maxr/x]_(i <- r | P i) F i = maxr x (\big[maxr/x]_(i <- r | P i) F i).
 Proof.
 rewrite -big_filter; elim: [seq i <- r | P i] => [|i l ihl].
-  by rewrite big_nil joinxx.
-by rewrite big_cons joinCA -ihl.
+  by rewrite big_nil maxxx.
+by rewrite big_cons maxCA -ihl.
 Qed.
 
 Lemma bigmaxrID I r (a P : pred I) (F : I -> {nonneg R}) x :
@@ -2156,10 +2156,10 @@ rewrite -!(big_filter _ (fun _ => _ && _)) !filter_andb !big_filter.
 rewrite ![in RHS](bigmaxr_mkcond _ _ F) !big_filter -bigmaxr_split.
 have eqmax : forall i, P i ->
   maxr (if a i then F i else x) (if ~~ a i then F i else x) = maxr (F i) x.
-  by move=> i _; case: (a i) => //=; rewrite joinC.
+  by move=> i _; case: (a i) => //=; rewrite maxC.
 rewrite [RHS](eq_bigr _ eqmax) -!(big_filter _ P).
 elim: [seq j <- r | P j] => [|j l ihl]; first by rewrite !big_nil.
-by rewrite !big_cons -joinA -bigmaxr_idl ihl.
+by rewrite !big_cons -maxA -bigmaxr_idl ihl.
 Qed.
 
 Lemma bigmaxr_seq1 I (i : I) (F : I -> {nonneg R}) x :
@@ -2178,13 +2178,13 @@ Lemma bigmaxrD1 (I : finType) j (P : pred I) (F : I -> {nonneg R}) x :
   P j -> \big[maxr/x]_(i | P i) F i
     = maxr (F j) (\big[maxr/x]_(i | P i && (i != j)) F i).
 Proof.
-move=> Pj; rewrite (bigmaxrID _ (pred1 j)) [in RHS]bigmaxr_idl joinA.
+move=> Pj; rewrite (bigmaxrID _ (pred1 j)) [in RHS]bigmaxr_idl maxA.
 by congr maxr; apply: bigmaxr_pred1 => i; rewrite /= andbC; case: eqP => //->.
 Qed.
 
 Lemma ler_bigmaxr_cond (I : finType) (P : pred I) (F : I -> {nonneg R}) x i0 :
   P i0 -> F i0 <= \big[maxr/x]_(i | P i) F i.
-Proof. by move=> Pi0; rewrite (bigmaxrD1 _ _ Pi0) lexU lexx. Qed.
+Proof. by move=> Pi0; rewrite (bigmaxrD1 _ _ Pi0) le_maxr lexx. Qed.
 
 Lemma ler_bigmaxr (I : finType) (F : I -> {nonneg R}) (i0 : I) x :
   F i0 <= \big[maxr/x]_i F i.
@@ -2195,8 +2195,8 @@ Lemma bigmaxr_lerP (I : finType) (P : pred I) m (F : I -> {nonneg R}) x :
     (\big[maxr/x]_(i | P i) F i <= m).
 Proof.
 apply: (iffP idP) => [|[lexm leFm]]; last first.
-  by elim/big_ind: _ => // ??; rewrite leUx =>->.
-rewrite bigmaxr_idl leUx => /andP[-> leFm]; split=> // i Pi.
+  by elim/big_ind: _ => // ??; rewrite le_maxl =>->.
+rewrite bigmaxr_idl le_maxl => /andP[-> leFm]; split=> // i Pi.
 by apply: le_trans leFm; apply: ler_bigmaxr_cond.
 Qed.
 
@@ -2209,8 +2209,8 @@ Lemma bigmaxr_ltrP (I : finType) (P : pred I) m (F : I -> {nonneg R}) x :
     (\big[maxr/x]_(i | P i) F i < m).
 Proof.
 apply: (iffP idP) => [|[ltxm ltFm]]; last first.
-  by elim/big_ind: _ => // ??; rewrite ltUx =>->.
-rewrite bigmaxr_idl ltUx => /andP[-> ltFm]; split=> // i Pi.
+  by elim/big_ind: _ => // ??; rewrite lt_maxl =>->.
+rewrite bigmaxr_idl lt_maxl => /andP[-> ltFm]; split=> // i Pi.
 by apply: le_lt_trans ltFm; apply: ler_bigmaxr_cond.
 Qed.
 
@@ -2219,8 +2219,8 @@ Lemma bigmaxr_gerP (I : finType) (P : pred I) m (F : I -> {nonneg R}) x :
   (m <= \big[maxr/x]_(i | P i) F i).
 Proof.
 apply: (iffP idP) => [|[lemx|[i Pi lemFi]]]; last 2 first.
-- by rewrite bigmaxr_idl lexU lemx.
-- by rewrite (bigmaxrD1 _ _ Pi) lexU lemFi.
+- by rewrite bigmaxr_idl le_maxr lemx.
+- by rewrite (bigmaxrD1 _ _ Pi) le_maxr lemFi.
 rewrite leNgt => /bigmaxr_ltrP /asboolPn.
 rewrite asbool_and negb_and => /orP [/asboolPn/negP|/existsp_asboolPn [i]].
   by rewrite -leNgt; left.
@@ -2232,8 +2232,8 @@ Lemma bigmaxr_gtrP (I : finType) (P : pred I) m (F : I -> {nonneg R}) x :
   (m < \big[maxr/x]_(i | P i) F i).
 Proof.
 apply: (iffP idP) => [|[ltmx|[i Pi ltmFi]]]; last 2 first.
-- by rewrite bigmaxr_idl ltxU ltmx.
-- by rewrite (bigmaxrD1 _ _ Pi) ltxU ltmFi.
+- by rewrite bigmaxr_idl lt_maxr ltmx.
+- by rewrite (bigmaxrD1 _ _ Pi) lt_maxr ltmFi.
 rewrite ltNge => /bigmaxr_lerP /asboolPn.
 rewrite asbool_and negb_and => /orP [/asboolPn/negP|/existsp_asboolPn [i]].
   by rewrite -ltNge; left.
@@ -2262,8 +2262,8 @@ Lemma bigmaxr_mkcond I r (P : pred I) (F : I -> R) x :
      \big[maxr/x]_(i <- r) (if P i then F i else x).
 Proof.
 rewrite unlock; elim: r x => //= i r ihr x.
-case P; rewrite ihr // join_r //; elim: r {ihr} => //= j r ihr.
-by rewrite lexU ihr orbT.
+case P; rewrite ihr // max_r //; elim: r {ihr} => //= j r ihr.
+by rewrite le_maxr ihr orbT.
 Qed.
 
 Lemma bigminr_maxr I r (P : pred I) (F : I -> R) x :
@@ -2284,8 +2284,8 @@ Lemma bigmaxr_split I r (P : pred I) (F1 F2 : I -> R) x :
   \big[maxr/x]_(i <- r | P i) (maxr (F1 i) (F2 i)) =
   maxr (\big[maxr/x]_(i <- r | P i) F1 i) (\big[maxr/x]_(i <- r | P i) F2 i).
 Proof.
-elim/big_rec3: _ => [|i y z _ _ ->]; rewrite ?joinxx //.
-by rewrite joinCA -!joinA joinCA.
+elim/big_rec3: _ => [|i y z _ _ ->]; rewrite ?maxxx //.
+by rewrite maxCA -!maxA maxCA.
 Qed.
 
 Lemma bigminr_split I r (P : pred I) (F1 F2 : I -> R) x :
@@ -2300,8 +2300,8 @@ Lemma bigmaxr_idl I r (P : pred I) (F : I -> R) x :
   \big[maxr/x]_(i <- r | P i) F i = maxr x (\big[maxr/x]_(i <- r | P i) F i).
 Proof.
 rewrite -big_filter; elim: [seq i <- r | P i] => [|i l ihl].
-  by rewrite big_nil joinxx.
-by rewrite big_cons joinCA -ihl.
+  by rewrite big_nil maxxx.
+by rewrite big_cons maxCA -ihl.
 Qed.
 
 Lemma bigminr_idl I r (P : pred I) (F : I -> R) x :
@@ -2317,10 +2317,10 @@ rewrite -!(big_filter _ (fun _ => _ && _)) !filter_andb !big_filter.
 rewrite ![in RHS](bigmaxr_mkcond _ _ F) !big_filter -bigmaxr_split.
 have eqmax : forall i, P i ->
   maxr (if a i then F i else x) (if ~~ a i then F i else x) = maxr (F i) x.
-  by move=> i _; case: (a i) => //=; rewrite joinC.
+  by move=> i _; case: (a i) => //=; rewrite maxC.
 rewrite [RHS](eq_bigr _ eqmax) -!(big_filter _ P).
 elim: [seq j <- r | P j] => [|j l ihl]; first by rewrite !big_nil.
-by rewrite !big_cons -joinA -bigmaxr_idl ihl.
+by rewrite !big_cons -maxA -bigmaxr_idl ihl.
 Qed.
 
 Lemma bigminrID I r (a P : pred I) (F : I -> R) x :
@@ -2357,7 +2357,7 @@ Lemma bigmaxrD1 (I : finType) j (P : pred I) (F : I -> R) x :
   P j -> \big[maxr/x]_(i | P i) F i
     = maxr (F j) (\big[maxr/x]_(i | P i && (i != j)) F i).
 Proof.
-move=> Pj; rewrite (bigmaxrID _ (pred1 j)) [in RHS]bigmaxr_idl joinA.
+move=> Pj; rewrite (bigmaxrID _ (pred1 j)) [in RHS]bigmaxr_idl maxA.
 by congr maxr; apply: bigmaxr_pred1 => i; rewrite /= andbC; case: eqP => //->.
 Qed.
 
@@ -2370,11 +2370,11 @@ Qed.
 
 Lemma ler_bigmaxr_cond (I : finType) (P : pred I) (F : I -> R) x i0 :
   P i0 -> F i0 <= \big[maxr/x]_(i | P i) F i.
-Proof. by move=> Pi0; rewrite (bigmaxrD1 _ _ Pi0) lexU lexx. Qed.
+Proof. by move=> Pi0; rewrite (bigmaxrD1 _ _ Pi0) le_maxr lexx. Qed.
 
 Lemma bigminr_ler_cond (I : finType) (P : pred I) (F : I -> R) x i0 :
   P i0 -> \big[minr/x]_(i | P i) F i <= F i0.
-Proof. by move=> Pi0; rewrite (bigminrD1 _ _ Pi0) leIx lexx. Qed.
+Proof. by move=> Pi0; rewrite (bigminrD1 _ _ Pi0) le_minl lexx. Qed.
 
 Lemma ler_bigmaxr (I : finType) (F : I -> R) (i0 : I) x :
   F i0 <= \big[maxr/x]_i F i.
@@ -2389,8 +2389,8 @@ Lemma bigmaxr_lerP (I : finType) (P : pred I) m (F : I -> R) x :
     (\big[maxr/x]_(i | P i) F i <= m).
 Proof.
 apply: (iffP idP) => [|[lexm leFm]]; last first.
-  by elim/big_ind: _ => // ??; rewrite leUx =>->.
-rewrite bigmaxr_idl leUx => /andP[-> leFm]; split=> // i Pi.
+  by elim/big_ind: _ => // ??; rewrite le_maxl =>->.
+rewrite bigmaxr_idl le_maxl => /andP[-> leFm]; split=> // i Pi.
 by apply: le_trans leFm; apply: ler_bigmaxr_cond.
 Qed.
 
@@ -2416,8 +2416,8 @@ Lemma bigmaxr_ltrP (I : finType) (P : pred I) m (F : I -> R) x :
     (\big[maxr/x]_(i | P i) F i < m).
 Proof.
 apply: (iffP idP) => [|[ltxm ltFm]]; last first.
-  by elim/big_ind: _ => // ??; rewrite ltUx =>->.
-rewrite bigmaxr_idl ltUx => /andP[-> ltFm]; split=> // i Pi.
+  by elim/big_ind: _ => // ??; rewrite lt_maxl =>->.
+rewrite bigmaxr_idl lt_maxl => /andP[-> ltFm]; split=> // i Pi.
 by apply: le_lt_trans ltFm; apply: ler_bigmaxr_cond.
 Qed.
 
@@ -2435,8 +2435,8 @@ Lemma bigmaxr_gerP (I : finType) (P : pred I) m (F : I -> R) x :
   (m <= \big[maxr/x]_(i | P i) F i).
 Proof.
 apply: (iffP idP) => [|[lemx|[i Pi lemFi]]]; last 2 first.
-- by rewrite bigmaxr_idl lexU lemx.
-- by rewrite (bigmaxrD1 _ _ Pi) lexU lemFi.
+- by rewrite bigmaxr_idl le_maxr lemx.
+- by rewrite (bigmaxrD1 _ _ Pi) le_maxr lemFi.
 rewrite leNgt => /bigmaxr_ltrP /asboolPn.
 rewrite asbool_and negb_and => /orP [/asboolPn/negP|/existsp_asboolPn [i]].
   by rewrite -leNgt; left.
@@ -2459,8 +2459,8 @@ Lemma bigmaxr_gtrP (I : finType) (P : pred I) m (F : I -> R) x :
   (m < \big[maxr/x]_(i | P i) F i).
 Proof.
 apply: (iffP idP) => [|[ltmx|[i Pi ltmFi]]]; last 2 first.
-- by rewrite bigmaxr_idl ltxU ltmx.
-- by rewrite (bigmaxrD1 _ _ Pi) ltxU ltmFi.
+- by rewrite bigmaxr_idl lt_maxr ltmx.
+- by rewrite (bigmaxrD1 _ _ Pi) lt_maxr ltmFi.
 rewrite ltNge => /bigmaxr_lerP /asboolPn.
 rewrite asbool_and negb_and => /orP [/asboolPn/negP|/existsp_asboolPn [i]].
   by rewrite -ltNge; left.
@@ -2543,10 +2543,10 @@ Proof. by []. Qed.
 
 Lemma ler_mx_norm_add x y : mx_norm (x + y) <= mx_norm x + mx_norm y.
 Proof.
-rewrite -nng_le; apply/BigmaxrNonneg.bigmaxr_lerP; split.
+rewrite nng_le; apply/BigmaxrNonneg.bigmaxr_lerP; split.
   exact: addr_ge0.
 move=> ij _; rewrite mxE; apply: le_trans (ler_norm_add _ _) _.
-rewrite ler_add // -nng_abs_le //= nng_le /= normr_id -nng_le;
+rewrite ler_add // -nng_abs_le //= -nng_le /= normr_id nng_le;
   exact/BigmaxrNonneg.ler_bigmaxr.
 Qed.
 
@@ -2554,13 +2554,13 @@ Lemma mx_norm_eq0 x : mx_norm x = 0 -> x = 0.
 Proof.
 move/eqP; rewrite eq_le => /andP [/BigmaxrNonneg.bigmaxr_lerP [_ x0] _].
 apply/matrixP => i j; rewrite mxE; apply/eqP.
-by rewrite -nng_abs_eq0 eq_le (x0 (i,j)) // andTb nng_le /= normr_ge0.
+by rewrite -nng_abs_eq0 eq_le (x0 (i,j)) // andTb -nng_le /= normr_ge0.
 Qed.
 
 Lemma mx_norm0 : mx_norm 0 = 0.
 Proof.
 rewrite /mx_norm (eq_bigr (fun=> 0%:nng)) /=.
-  by elim/big_ind : _ => // a b /val_inj ->{a} /val_inj ->{b}; rewrite joinxx.
+  by elim/big_ind : _ => // a b /val_inj ->{a} /val_inj ->{b}; rewrite maxxx.
 by move=> i _; apply val_inj => /=; rewrite mxE normr0.
 Qed.
 
@@ -2570,9 +2570,9 @@ rewrite /mx_norm.
 elim/big_ind : _ => [|a b Ha Hb H|/= i _ _]; [by rewrite eqxx| |by exists i].
 case: (leP a b) => ab.
 + suff /Hb[i xi] : b != 0%:nng by exists i.
-  by apply: contra H => b0; rewrite join_r.
+  by apply: contra H => b0; rewrite max_r.
 + suff /Ha[i xi] : a != 0%:nng by exists i.
-  by apply: contra H => a0; rewrite join_l // ltW.
+  by apply: contra H => a0; rewrite max_l // ltW.
 Qed.
 
 Lemma mx_norm_natmul x k : mx_norm (x *+ k) = (mx_norm x) *+ k.
@@ -2592,7 +2592,7 @@ Qed.
 Lemma mx_normN x : mx_norm (- x) = mx_norm x.
 Proof.
 congr (_%:nngnum).
-by apply eq_bigr => /= ? _; apply/eqP; rewrite mxE nng_eq //= normrN.
+by apply eq_bigr => /= ? _; apply/eqP; rewrite mxE -nng_eq //= normrN.
 Qed.
 
 End mx_norm.
@@ -2602,7 +2602,7 @@ Lemma mx_normrE (K : realDomainType) (m n : nat) (x : 'M[K]_(m, n)) :
 Proof.
 rewrite /mx_norm; apply/esym.
 elim/big_ind2 : _ => //= a a' b b' ->{a'} ->{b'}.
-case: (leP a b) => ab; by [rewrite join_r | rewrite join_l // ltW].
+case: (leP a b) => ab; by [rewrite max_r | rewrite max_l // ltW].
 Qed.
 
 Definition matrix_normedZmodMixin (K : numDomainType) (m n : nat) :=
@@ -2623,8 +2623,8 @@ rewrite /= /normr /= predeq3E => x e y; split.
   (* TODO:  lemma : ball x e y -> 0 < e *)
   have lee0 : ( 0 < e) by rewrite (le_lt_trans _ (xe_y ord0 ord0)) //.
   have -> : e = (Nonneg.NngNum _ (ltW lee0))%:nngnum by [].
-  rewrite -nng_lt; apply/BigmaxrNonneg.bigmaxr_ltrP.
-- split; [rewrite nng_lt //= | move=> ??; rewrite !mxE; exact: xe_y].
+  rewrite nng_lt; apply/BigmaxrNonneg.bigmaxr_ltrP.
+- split; [rewrite -nng_lt //= | move=> ??; rewrite !mxE; exact: xe_y].
   rewrite /ball_; rewrite mx_normE => H.
   have lee0 : (0 < e) by rewrite (le_lt_trans _ H) // nonnegnum_ge0.
   move : H.
@@ -2642,7 +2642,7 @@ Lemma mx_normZ (l : K) (x : 'M[K]_(m.+1, n.+1)) : `| l *: x | = `| l | * `| x |.
 Proof.
 rewrite {1 3}/normr /= !mx_normE
  (eq_bigr (fun i => (`|l| * `|x i.1 i.2|)%:nng)); last first.
-  by move=> i _; rewrite mxE //=; apply/eqP; rewrite nng_eq /= normrM.
+  by move=> i _; rewrite mxE //=; apply/eqP; rewrite -nng_eq /= normrM.
 elim/big_ind2 : _ => // [|a b c d bE dE]; first by rewrite mulr0.
 rewrite nonneg_maxr; congr (maxr _ _)%:nngnum; exact/val_inj.
 Qed.
@@ -2658,21 +2658,14 @@ End matrix_NormedModule.
 Section prod_NormedModule.
 Context {K : numDomainType} {U V : normedModType K}.
 
-Lemma prod_normE (x : U * V) : `| x | =
-  (Num.max `| x.1 |%:nng `|x.2|%:nng)%:nngnum.
-Proof. by []. Qed.
-
 Lemma prod_norm_scale (l : K) (x : U * V) : `| l *: x | = `|l| * `| x |.
-Proof.
-rewrite prod_normE /= nonneg_maxr /=.
-by congr (maxr _ _ )%:nngnum; apply val_inj => /=; rewrite normmZ.
-Qed.
+Proof. by rewrite prod_normE /= !normmZ maxr_pmulr. Qed.
 
 Lemma ball_prod_normE : ball = ball_ (fun x => `| x : U * V |).
 Proof.
 rewrite funeq2E => - [xu xv] e; rewrite predeqE => - [yu yv].
 rewrite /ball /= /prod_ball -!ball_normE /ball_ /=.
-by rewrite nng_ltUx /=; split=> /andP.
+by rewrite comparable_lt_maxl// ?real_comparable//; split=> /andP.
 Qed.
 
 Lemma prod_norm_ball : @ball _ [pseudoMetricType K of U * V] = ball_ (fun x => `|x|).
@@ -3268,7 +3261,7 @@ Section TODO_add_to_ssrnum.
 Lemma maxr_real (K : realDomainType) (x y : K) :
   x \is Num.real -> y \is Num.real -> maxr x y \is Num.real.
 Proof.
-by rewrite !realE => /orP[|] x0 /orP[|] y0; rewrite lexU leUx x0 y0 !(orbT,orTb).
+by rewrite !realE => /orP[|] x0 /orP[|] y0; rewrite le_maxr le_maxl x0 y0 !(orbT,orTb).
 Qed.
 
 Lemma bigmaxr_real (K : realDomainType) (R : choiceType) (x : K) (D : seq R) (f : R -> K):
@@ -3428,17 +3421,17 @@ suff [t Altxt] : exists2 t, Altx t & z < t.
 exists (z + (minr (e%:num / 2) ((PosNum ltzx)%:num / 2))); last first.
   by rewrite ltr_addl.
 rewrite inE; split; last first.
-  rewrite -[_ < _]ltr_subr_addl ltIx; apply/orP; right.
+  rewrite -[_ < _]ltr_subr_addl lt_minl; apply/orP; right.
   by rewrite ltr_pdivr_mulr // mulrDr mulr1 ltr_addl.
 rewrite AeabC; split; last first.
   apply: ze_C; rewrite /ball_ ltr_distl.
   apply/andP; split; last by rewrite -addrA ltr_addl.
-  rewrite -addrA gtr_addl subr_lt0 ltIx; apply/orP; left.
+  rewrite -addrA gtr_addl subr_lt0 lt_minl; apply/orP; left.
   by rewrite [X in _ < X]splitr ltr_addl.
 rewrite inE; apply/andP; split.
   by apply: ler_paddr => //; have := Az; rewrite AeabB => - [/itvP->].
 have : x <= b by rewrite (itvP abx).
-apply: le_trans; rewrite -ler_subr_addl leIx; apply/orP; right.
+apply: le_trans; rewrite -ler_subr_addl le_minl; apply/orP; right.
 by rewrite ler_pdivr_mulr // mulrDr mulr1 ler_addl; apply: ltW.
 Qed.
 
@@ -3517,16 +3510,13 @@ Lemma IVT (R : realType) (f : R^o -> R^o) (a b v : R^o) :
   minr (f a) (f b) <= v <= maxr (f a) (f b) ->
   exists2 c, c \in `[a, b] & f c = v.
 Proof.
-move=> leab; wlog : f v / f a <= f b.
-  move=> ivt; case: (lerP (f a) (f b)) => [|/ltW lefba].
-    exact: ivt.
-  move=> fcont fabv; have [] := ivt (fun x => - f x) (- v).
-  - by rewrite ler_oppr opprK.
-  - by move=> x /fcont; apply: (@continuousN _ [normedModType R of R^o]).
-  - by rewrite -oppr_max -oppr_min ler_oppr opprK ler_oppr opprK andbC.
-  by move=> c cab /eqP; rewrite eqr_opp => /eqP; exists c.
-move=> lefab fcont; rewrite meet_l // join_r // => /andP [].
-rewrite le_eqVlt => /orP [/eqP<- _|ltfav].
+move=> leab fcont; gen have ivt : f v fcont / f a <= v <= f b ->
+    exists2 c, c \in `[a, b] & f c = v; last first.
+  case: (leP (f a) (f b)) => [] _ fabv; first exact: ivt.
+  have [||c cab /oppr_inj] := ivt (- f) (- v); last by exists c.
+    by move=> x /fcont; apply: (@continuousN _ [normedModType R of R^o]).
+  by rewrite ler_oppr opprK ler_oppr opprK andbC.
+move=> /andP[]; rewrite le_eqVlt => /orP [/eqP<- _|ltfav].
   by exists a => //; rewrite inE/= lexx leab.
 rewrite le_eqVlt => /orP [/eqP->|ltvfb].
   by exists b => //; rewrite inE/= lexx leab.
@@ -3581,8 +3571,8 @@ move=> [:wlog]; case: a b => [a||] [b||] //= ltax ltxb.
 - move: a b ltax ltxb; abstract: wlog. (*BUG*)
   move=> {a b} a b ltxa ltxb.
   have m_gt0 : (minr ((x - a) / 2) ((b - x) / 2) > 0).
-    by rewrite ltxI !divr_gt0 // ?subr_gt0.
-  exists (PosNum m_gt0) => y //=; rewrite ltxI !ltr_distl.
+    by rewrite lt_minr !divr_gt0 // ?subr_gt0.
+  exists (PosNum m_gt0) => y //=; rewrite lt_minr !ltr_distl.
   move=> /andP[/andP[ay _] /andP[_ yb]].
   rewrite 2!lte_fin (lt_trans _ ay) ?(lt_trans yb) //=.
     by rewrite -subr_gt0 opprD addrA {1}[b - x]splitr addrK divr_gt0 ?subr_gt0.
@@ -4039,15 +4029,15 @@ Proof.
 move=> P; rewrite /ereal_loc_seq.
 case: x => /= [x [_/posnumP[d] Hp] |[d [dreal Hp]] |[d [dreal Hp]]]; last 2 first.
     have /ZnatP [N Nfloor] : ifloor (maxr d 0) \is a Znat.
-      by rewrite Znat_def ifloor_ge0 lexU lexx orbC.
+      by rewrite Znat_def ifloor_ge0 le_maxr lexx orbC.
     exists N.+1 => // n ltNn; apply: Hp.
-    have /le_lt_trans : d <= maxr d 0 by rewrite lexU lexx.
+    have /le_lt_trans : d <= maxr d 0 by rewrite le_maxr lexx.
     apply; apply: lt_le_trans (floorS_gtr _) _; rewrite floorE Nfloor.
     by rewrite -(@natrD R N 1) ler_nat addn1.
   have /ZnatP [N Nfloor] : ifloor (maxr (- d) 0) \is a Znat.
-    by rewrite Znat_def ifloor_ge0 lexU lexx orbC.
+    by rewrite Znat_def ifloor_ge0 le_maxr lexx orbC.
   exists N.+1 => // n ltNn; apply: Hp; rewrite lte_fin ltr_oppl.
-  have /le_lt_trans : - d <= maxr (- d) 0 by rewrite lexU lexx.
+  have /le_lt_trans : - d <= maxr (- d) 0 by rewrite le_maxr lexx.
   apply; apply: lt_le_trans (floorS_gtr _) _; rewrite floorE Nfloor.
   by rewrite -(@natrD R N 1) ler_nat addn1.
 have /ZnatP [N Nfloor] : ifloor (d%:num^-1) \is a Znat.
diff --git a/theories/posnum.v b/theories/posnum.v
index c7e28bb44d..0ba786fe49 100644
--- a/theories/posnum.v
+++ b/theories/posnum.v
@@ -66,6 +66,7 @@ Notation "'{posnum' R }" := (posnum_of (@Phant R)).
 Definition PosNum (R : numDomainType) x x_gt0 : {posnum R} :=
   @PosNumDef _ (Phant R) x x_gt0.
 
+Notation numpos R := (@num_of_pos _ (Phant R)).
 Notation "x %:num" := (num_of_pos x) : ring_scope.
 Definition pos_of_num (R : numDomainType) (x : {posnum R})
    (phx : phantom R x%:num) := x.
@@ -95,7 +96,7 @@ End Order.
 
 Section PosNum.
 Context {R : numDomainType}.
-Implicit Types (x y : {posnum R}).
+Implicit Types (x y : {posnum R}) (a b : R).
 
 Definition posnum_gt0_def x (phx : phantom R x%:num) := posnum_gt0 x.
 
@@ -103,13 +104,21 @@ Lemma posnum_ge0 x : x%:num >= 0 :> R. Proof. by apply: ltW. Qed.
 Lemma posnum_eq0 x : (x%:num == 0 :> R) = false. Proof. by rewrite gt_eqF. Qed.
 Lemma posnum_neq0 x : (x%:num != 0 :> R). Proof. by rewrite gt_eqF. Qed.
 
-Lemma add_pos_gt0 x y : 0 < x%:num + y%:num.
-Proof. by rewrite addr_gt0. Qed.
-Canonical addr_posnum x y := PosNum (add_pos_gt0 x y).
+Lemma posnum_eq : {mono numpos R : x y / x == y}. Proof. by []. Qed.
+Lemma posnum_le : {mono numpos R : x y / x <= y}. Proof. by []. Qed.
+Lemma posnum_lt : {mono numpos R : x y / x < y}. Proof. by []. Qed.
 
-Lemma mul_pos_posnum x y : 0 < x%:num * y%:num.
-Proof. by rewrite mulr_gt0. Qed.
-Canonical mulr_posnum x y := PosNum (mul_pos_posnum x y).
+Lemma posnum_min : {morph numpos R : x y / Order.min x y}.
+Proof. by move=> x y; rewrite !minEle posnum_le -fun_if. Qed.
+
+Lemma posnum_max : {morph numpos R : x y / Order.max x y}.
+Proof. by move=> x y; rewrite !maxEle posnum_le -fun_if. Qed.
+
+Lemma posnum_real x : x%:num \is Num.real. Proof. by rewrite gtr0_real. Qed.
+Hint Resolve posnum_real.
+
+Canonical addr_posnum x y := PosNum (addr_gt0 x y).
+Canonical mulr_posnum x y := PosNum (mulr_gt0 x y).
 
 Lemma muln_pos_posnum x n : 0 < x%:num *+ n.+1.
 Proof. by rewrite pmulrn_lgt0. Qed.
@@ -127,41 +136,23 @@ Proof. by rewrite lt_geF. Qed.
 Lemma posnum_lt0 x : (x%:num < 0 :> R) = false.
 Proof. by rewrite lt_gtF. Qed.
 
-Lemma pos_ltUx (a : R) x y : (Num.max x y)%:num < a = (x%:num < a) && (y%:num < a).
-Proof.
-case: (lcomparable_ltgtP (comparableT x y)) => [?|?|<-]; last by rewrite andbb.
-rewrite andb_idl //; exact/lt_trans.
-rewrite andb_idr //; exact/lt_trans.
-Qed.
+Lemma pos_lt_maxl a x y : Num.max x%:num y%:num < a = (x%:num < a) && (y%:num < a).
+Proof. by rewrite comparable_lt_maxl ?real_comparable. Qed.
 
-Lemma pos_ltxI (a : R) x y : a < (Num.min x y)%:num = (a < x%:num) && (a < y%:num).
-Proof.
-case: (ltP x y)=> ?.
-by rewrite andb_idr // => /lt_trans; apply.
-by rewrite andb_idl // => /lt_le_trans; apply.
-Qed.
-
-End PosNum.
-Hint Extern 0 ((0 <= _)%R = true) => exact: posnum_ge0 : core.
-Hint Extern 0 ((_ != 0)%R = true) => exact: posnum_neq0 : core.
-
-Section PosNumReal.
-Context {R : realDomainType}.
-Implicit Types (x y : {posnum R}).
-
-Lemma min_posE x y : Num.min x%:num y%:num = (Num.min x y)%:num.
-Proof.
-case: (lcomparable_ltgtP (comparableT x y)) => [yx|xy|<-]; last first.
-- by rewrite meetxx.
-- by rewrite (meet_idPr _)// ltW.
-- by rewrite (meet_idPl _)// ltW.
-Qed.
+Lemma pos_lt_minr (a : R) x y : a < Num.min x%:num y%:num = (a < x%:num) && (a < y%:num).
+Proof. by rewrite comparable_lt_minr ?real_comparable. Qed.
 
 Lemma min_pos_gt0 x y : 0 < Num.min x%:num y%:num.
-Proof. by rewrite ltxI !posnum_gt0. Qed.
+Proof. by rewrite -posnum_min !posnum_gt0. Qed.
 Canonical minr_posnum x y := PosNum (@min_pos_gt0 x y).
 
-End PosNumReal.
+Lemma max_pos_gt0 x y : 0 < Num.max x%:num y%:num.
+Proof. by rewrite -posnum_max !posnum_gt0. Qed.
+Canonical maxr_posnum x y := PosNum (@max_pos_gt0 x y).
+
+End PosNum.
+Hint Extern 0 ((0 <= _)%R = true) => solve [apply: posnum_ge0] : core.
+Hint Extern 0 ((_ != 0)%R = true) => solve [apply: posnum_neq0] : core.
 
 Lemma sqrt_pos_gt0 (R : rcfType) (x : {posnum R}) : 0 < Num.sqrt (x%:num).
 Proof. by rewrite sqrtr_gt0. Qed.
diff --git a/theories/prodnormedzmodule.v b/theories/prodnormedzmodule.v
index 102795928f..188ae69441 100644
--- a/theories/prodnormedzmodule.v
+++ b/theories/prodnormedzmodule.v
@@ -60,6 +60,7 @@ End nonnegative_numbers.
 Module Exports.
 Arguments NngNum {R}.
 Notation "'{nonneg' R }" := (nngnum_of (@Phant R)) : type_scope.
+Notation nngnum R := (@num_of_nng _ (@Phant R)).
 Notation "x %:nngnum" := (num_of_nng x) : ring_scope.
 Hint Extern 0 ((0 <= _)%R = true) => exact: nngnum_ge0 : core.
 Notation "x %:nng" := (nng_of_num (Phantom _ x)) : ring_scope.
@@ -81,76 +82,72 @@ Implicit Types x y : {nonneg R}.
 Import Nonneg.
 
 Canonical addr_nngnum x y := NngNum (x%:nngnum + y%:nngnum) (addr_ge0 x y).
-
 Canonical mulr_nngnum x y := NngNum (x%:nngnum * y%:nngnum) (mulr_ge0 x y).
-
 Canonical mulrn_nngnum x n := NngNum (x%:nngnum *+ n) (mulrn_wge0 n x).
-
 Canonical zeror_nngnum := @NngNum R 0 (lexx 0).
 Canonical oner_nngnum := @NngNum R 1 ler01.
 
 Lemma nngnum_lt0 x : (x%:nngnum < 0 :> R) = false.
 Proof. by rewrite le_gtF. Qed.
 
-Lemma nng_eq0 x : (x == 0%:nng) = (x%:nngnum == 0).
-Proof. by []. Qed.
+Lemma nngnum_real x : x%:nngnum \is Num.real.
+Proof. by rewrite ger0_real. Qed.
+Hint Resolve nngnum_real.
 
-Lemma nng_eq x y : (x == y) = (x%:nngnum == y%:nngnum).
-Proof. by []. Qed.
+Lemma nng_eq : {mono nngnum R : x y / x == y}. Proof. by []. Qed.
+Lemma nng_le : {mono nngnum R : x y / x <= y}. Proof. by []. Qed.
+Lemma nng_lt : {mono nngnum R : x y / x < y}. Proof. by []. Qed.
 
-Lemma nng_le x y : (x <= y) = (x%:nngnum <= y%:nngnum).
+Lemma nng_eq0 x : (x%:nngnum == 0) = (x == 0%:nng).
 Proof. by []. Qed.
 
-Lemma nng_lt x y : (x < y) = (x%:nngnum < y%:nngnum).
-Proof. by []. Qed.
+Lemma nng_min : {morph nngnum R : x y / Order.min x y}.
+Proof. by move=> x y; rewrite !minEle nng_le -fun_if. Qed.
 
-Lemma nng_lexU a x y :
-  a <= (Num.max x y)%:nngnum = (a <= x%:nngnum) || (a <= y%:nngnum).
-Proof.
-case: (leP x y)=> ?.
-rewrite orb_idl // => /le_trans; exact.
-rewrite orb_idr // => /le_trans; apply; exact/ltW.
-Qed.
+Lemma nng_max : {morph nngnum R : x y / Order.max x y}.
+Proof. by move=> x y; rewrite !maxEle nng_le -fun_if. Qed.
 
-Lemma nng_leUx a x y :
-  (Num.max x y)%:nngnum <= a = (x%:nngnum <= a) && (y%:nngnum <= a).
-Proof.
-case: (leP x y)=> ?.
-rewrite andb_idl //; exact/le_trans.
-rewrite andb_idr //; exact/le_trans/ltW.
-Qed.
+Lemma nng_le_maxr a x y :
+  a <= Num.max x%:nngnum y%:nngnum = (a <= x%:nngnum) || (a <= y%:nngnum).
+Proof. by rewrite -comparable_le_maxr// real_comparable. Qed.
 
-Lemma nng_ltUx a x y :
-  (Num.max x y)%:nngnum < a = (x%:nngnum < a) && (y%:nngnum < a).
-Proof.
-case: leP=> ?.
-rewrite andb_idl //; exact/le_lt_trans.
-rewrite andb_idr //; exact/lt_trans.
-Qed.
+Lemma nng_le_maxl a x y :
+  Num.max x%:nngnum  y%:nngnum <= a = (x%:nngnum <= a) && (y%:nngnum <= a).
+Proof. by rewrite -comparable_le_maxl// real_comparable. Qed.
+
+Lemma nng_le_minr a x y :
+  a <= Num.min x%:nngnum y%:nngnum = (a <= x%:nngnum) && (a <= y%:nngnum).
+Proof. by rewrite -comparable_le_minr// real_comparable. Qed.
+
+Lemma nng_le_minl a x y :
+  Num.min x%:nngnum y%:nngnum <= a = (x%:nngnum <= a) || (y%:nngnum <= a).
+Proof. by rewrite -comparable_le_minl// real_comparable. Qed.
 
-Canonical normr_nngnum (V : normedZmodType R) (x : V) := NngNum `|x| (normr_ge0 x).
+Lemma max_ge0 x y : Num.max x%:nngnum y%:nngnum >= 0.
+Proof. by rewrite comparable_le_maxr ?real_comparable// ?nngnum_ge0. Qed.
+
+Lemma min_ge0 x y : Num.min x%:nngnum y%:nngnum >= 0.
+Proof. by rewrite comparable_le_minr ?real_comparable// ?nngnum_ge0. Qed.
+
+Canonical max_nngnum x y := NngNum (Num.max x%:nngnum y%:nngnum) (max_ge0 x y).
+Canonical min_nngnum x y := NngNum (Num.min x%:nngnum y%:nngnum) (min_ge0 x y).
+
+Canonical normr_nngnum (V : normedZmodType R) (x : V) :=
+  NngNum `|x| (normr_ge0 x).
 
 Lemma nng_abs_eq0 a : (`|a|%:nng == 0%:nng) = (a == 0).
 Proof. by rewrite -normr_eq0. Qed.
 
 Lemma nng_abs_le a x : 0 <= a -> (`|a|%:nng <= x) = (a <= x%:nngnum).
-Proof.
-move=> a0; case: (leP _ x); first by rewrite nng_le /= ger0_norm.
-rewrite ltNge => ax; apply/esym; apply: contraNF ax => ax.
-by rewrite nng_le /= ger0_norm.
-Qed.
+Proof. by move=> a0; rewrite -nng_le//= ger0_norm. Qed.
 
 Lemma nng_abs_lt a x : 0 <= a -> (`|a|%:nng < x) = (a < x%:nngnum).
-Proof.
-by move=> ?; rewrite lt_neqAle nng_abs_le // lt_neqAle nng_eq /= ger0_norm.
-Qed.
+Proof. by move=> a0; rewrite -nng_lt/= ger0_norm. Qed.
 
+(* Cyril: remove *)
 Lemma nonneg_maxr a x y : `|a| * (Num.max x y)%:nngnum =
   (Num.max (`|a| * x%:nngnum)%:nng (`|a| * y%:nngnum)%:nng)%:nngnum.
-Proof.
-move: x y; apply: wlog_le => x y hxy; first by rewrite joinC hxy joinC.
-rewrite !join_r //; exact/ler_wpmul2l.
-Qed.
+Proof. by rewrite !nng_max maxr_pmulr. Qed.
 
 End NngNum.
 
@@ -162,33 +159,25 @@ Module ProdNormedZmodule.
 Section ProdNormedZmodule.
 Context {R : numDomainType} {U V : normedZmodType R}.
 
-Definition norm (x : U * V) : R := (Num.max (`| x.1 |%:nng) (`|x.2|%:nng))%:nngnum.
+Definition norm (x : U * V) : R := Num.max `|x.1| `|x.2|.
 
 Lemma normD x y : norm (x + y) <= norm x + norm y.
 Proof.
-rewrite /norm nng_leUx /=; apply/andP; split;
-  case: leP => [|/ltW] Hx; case: leP => [|/ltW] Hy;
-  exact/(le_trans (ler_norm_add _ _))/ler_add.
+rewrite /norm nng_le_maxl !(le_trans (ler_norm_add _ _)) ?ler_add//;
+by rewrite comparable_le_maxr ?lexx ?orbT// real_comparable.
 Qed.
 
 Lemma norm_eq0 x : norm x = 0 -> x = 0.
 Proof.
-case: x=> x1 x2 /eqP; rewrite eq_le nng_leUx 2!normr_le0 -andbA /=.
+case: x => x1 x2 /eqP; rewrite eq_le nng_le_maxl 2!normr_le0 -andbA/=.
 by case/and3P => /eqP -> /eqP ->.
 Qed.
 
 Lemma normMn x n : norm (x *+ n) = (norm x) *+ n.
-Proof.
-by rewrite /norm pairMnE /=; case: leP => [|/ltW];
-  rewrite nng_le /= !normrMn ler_muln2r => /predU1P [->|];
-  rewrite ?mulr0n // -nng_le; [case: leP | case: ltP].
-Qed.
+Proof. by rewrite /norm pairMnE -mulr_natl maxr_pmulr ?mulr_natl ?normrMn. Qed.
 
 Lemma normrN x : norm (- x) = norm x.
-Proof.
-by rewrite /norm /=; case: leP => [|/ltW];
-  rewrite nng_le /= !normrN -nng_le; [case: leP | case: ltP].
-Qed.
+Proof. by rewrite /norm/= !normrN. Qed.
 
 Definition normedZmodMixin :
   @Num.normed_mixin_of R [zmodType of U * V] (Num.NumDomain.class R) :=
@@ -196,8 +185,7 @@ Definition normedZmodMixin :
 
 Canonical normedZmodType := NormedZmodType R (U * V) normedZmodMixin.
 
-Lemma prod_normE (x : normedZmodType) :
-  `| x | = (Num.max `| x.1 |%:nng `|x.2|%:nng)%:nngnum.
+Lemma prod_normE (x : normedZmodType) : `|x| = Num.max `|x.1| `|x.2|.
 Proof. by []. Qed.
 
 End ProdNormedZmodule.
diff --git a/theories/sequences.v b/theories/sequences.v
index 4dee943bef..3f2de3f617 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -179,8 +179,8 @@ split => [u_cvg _/posnumP[A]|u_ge X [A [Ar AX]]].
   by apply: u_cvg; apply: locally_pinfty_ge.
 rewrite !near_simpl [\near u_, X _](near_map u_ \oo); near=> x.
 apply: AX; rewrite (@lt_le_trans _ _ ((maxr 0 A) +1)) //.
-  by rewrite ltr_spaddr // lexU lexx orbT.
-by near: x; apply: u_ge; rewrite ltr_spaddr // lexU lexx.
+  by rewrite ltr_spaddr // le_maxr lexx orbT.
+by near: x; apply: u_ge; rewrite ltr_spaddr // le_maxr lexx.
 Grab Existential Variables. all: end_near. Qed.
 
 Lemma cvgNpinfty (u_ : R^o ^nat) : (- u_ --> +oo) = (u_ --> -oo).
@@ -407,10 +407,10 @@ Lemma near_nondecreasing_is_cvg (u_ : (R^o) ^nat) (M : R) :
     (\forall n \near \oo, u_ n <= M) ->
   cvg u_.
 Proof.
-move=> [k _ u_nd] [k' _ u_M]; suff : cvg [sequence u_ (n + max k k')%N]_n.
+move=> [k _ u_nd] [k' _ u_M]; suff : cvg [sequence u_ (n + maxn k k')%N]_n.
   by case/cvg_ex => /= l; rewrite cvg_comp_addn => ul; apply/cvg_ex; exists l.
-apply (@nondecreasing_is_cvg _ M) => [? ? ? | ?].
-by rewrite u_nd ?leq_add2r ?(leq_trans (leq_maxl _ _) (leq_addl _ _)).
+apply (@nondecreasing_is_cvg _ M) => [/= ? ? ? | ?].
+  by rewrite u_nd ?leq_add2r ?(leq_trans (leq_maxl _ _) (leq_addl _ _))//.
 by rewrite u_M // (leq_trans (leq_maxr _ _) (leq_addl _ _)).
 Qed.
 
diff --git a/theories/topology.v b/theories/topology.v
index 26fd81a04a..6cf34f5cd7 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -2728,7 +2728,7 @@ rewrite (PseudoMetric.ax4 m) locally_E; apply filter_from_proper; last first.
   exact: PseudoMetric.ax1.
 apply: filter_from_filter => [|_ _ /posnumP[e1] /posnumP[e2]]; first by exists 1.
 exists (Num.min e1 e2)%:num; rewrite ?subsetI//.
-by split=> //; apply: my_ball_le; rewrite -leEsub leIx lexx ?orbT.
+by split=> //; apply: my_ball_le; rewrite -leEsub le_minl lexx ?orbT.
 Qed.
 Next Obligation.
 move=> R T loc m p A; rewrite (PseudoMetric.ax4 m) locally_E => - [_/posnumP[e]]; apply.
@@ -2807,7 +2807,7 @@ Proof.
 apply filter_from_proper; last by exists (point,point); apply: ballxx.
 apply: filter_from_filter; first by exists 1; rewrite ltr01.
 move=> _ _ /posnumP[i] /posnumP[j]; exists (Num.min i j)%:num; rewrite ?subsetI//.
-by split=> // ?; apply: ball_ler; rewrite -leEsub leIx lexx ?orbT.
+by split=> // ?; apply: ball_ler; rewrite -leEsub le_minl lexx ?orbT.
 Qed.
 Typeclasses Opaque entourages.
 
@@ -2977,7 +2977,7 @@ Lemma ltr_bigminr (I : finType) (f : I -> {posnum R}) (x0 x : {posnum R}) :
   x < x0 -> (forall i, x < f i) -> x < \big[Num.min/x0]_i f i.
 Proof.
 move=> ltx0 ltxf; elim/big_ind: _ => // y z ltxy ltxz.
-by rewrite ltxI ltxy ltxz.
+by rewrite lt_minr ltxy ltxz.
 Qed.
 
 (* TODO: see bigminr_ler in normedtype.v *)
@@ -2986,7 +2986,7 @@ Lemma bigminr_ler (I : finType) (f : I -> {posnum R}) (x0 : {posnum R}) i :
 Proof.
 have := mem_index_enum i; rewrite unlock; elim: (index_enum I) => //= j l ihl.
 by rewrite inE => /orP [/eqP->|/ihl leminlfi];
-  rewrite leIx ?lexx // leminlfi orbC.
+  rewrite le_minl ?lexx // leminlfi orbC.
 Qed.
 
 Canonical R_pointedType := PointedType R 0.
@@ -3031,8 +3031,8 @@ rewrite predeq2E => -[x y] P; split=> [[[A B] /=[xX yY] XYP] |]; last first.
   by move=> [_ /posnumP[eps] epsP]; exists (ball x eps%:num, ball y eps%:num) => /=.
 move: xX yY => /locallyP [_ /posnumP[ex] eX] /locallyP [_ /posnumP[ey] eY].
 exists (Num.min ex ey)%:num => // -[x' y'] [/= xx' yy']; apply: XYP; split=> /=.
-  by apply/eX/(ball_ler _ xx'); rewrite -leEsub leIx lexx.
-by apply/eY/(ball_ler _ yy'); rewrite -leEsub leIx lexx orbT.
+  by apply/eX/(ball_ler _ xx'); rewrite -leEsub le_minl lexx.
+by apply/eY/(ball_ler _ yy'); rewrite -leEsub le_minl lexx orbT.
 Qed.
 Definition prod_pseudoMetricType_mixin :=
   PseudoMetric.Mixin prod_ball_center prod_ball_sym prod_ball_triangle prod_locally.