diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index fcc3ca580..8acf8ff94 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -73,6 +73,26 @@
 - in `classical_sets.v`:
   + `notin_set` -> `notin_setE`
 
+- in `signed.v`:
+  + `num_le_maxr` -> `num_le_max`
+  + `num_le_maxl` -> `num_ge_max`
+  + `num_le_minr` -> `num_le_min`
+  + `num_le_minl` -> `num_ge_min`
+  + `num_lt_maxr` -> `num_lt_max`
+  + `num_lt_maxl` -> `num_gt_max`
+  + `num_lt_minr` -> `num_lt_min`
+  + `num_lt_minl` -> `num_gt_min`
+
+- in `constructive_ereal.v`:
+  + `num_lee_maxr` -> `num_lee_max`
+  + `num_lee_maxl` -> `num_gee_max`
+  + `num_lee_minr` -> `num_lee_min`
+  + `num_lee_minl` -> `num_gee_min`
+  + `num_lte_maxr` -> `num_lte_max`
+  + `num_lte_maxl` -> `num_gte_max`
+  + `num_lte_minr` -> `num_lte_min`
+  + `num_lte_minl` -> `num_gte_min`
+
 ### Generalized
 
 - in `constructive_ereal.v`:
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index 98dee74c5..bbec2949a 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -155,8 +155,8 @@ Lemma le_bigmax_seq F :
   i0 \in r -> P i0 -> (F i0 <= \big[Order.max/x]_(i <- r | P i) F i)%O.
 Proof.
 move=> + Pi0; elim: r => // h t ih; rewrite inE big_cons.
-move=> /predU1P[<-|i0t]; first by rewrite Pi0 le_maxr// lexx.
-by case: ifPn => Ph; [rewrite le_maxr ih// orbT|rewrite ih].
+move=> /predU1P[<-|i0t]; first by rewrite Pi0 le_max// lexx.
+by case: ifPn => Ph; [rewrite le_max ih// orbT|rewrite ih].
 Qed.
 
 (* NB: as of [2023-08-28], bigop.bigmax_sup_seq already exists for nat *)
diff --git a/classical/set_interval.v b/classical/set_interval.v
index c3c7caf89..ae2387d38 100644
--- a/classical/set_interval.v
+++ b/classical/set_interval.v
@@ -341,8 +341,8 @@ move: a => [b r|[|]] _ //.
   suff: ~ has_lbound `]-oo, r[%classic.
     by case: b => //; apply/contra_not/subset_has_lbound => x /ltW.
   apply/has_lbPn => x; exists (minr (r - 1) (x - 1)).
-    by rewrite !set_itvE/= lt_minl ltrBlDr ltrDl ltr01.
-  by rewrite lt_minl orbC ltrBlDr ltrDl ltr01.
+    by rewrite !set_itvE/= gt_min ltrBlDr ltrDl ltr01.
+  by rewrite gt_min orbC ltrBlDr ltrDl ltr01.
 case=> r /(_ (r - 1)) /=; rewrite in_itv /= => /(_ erefl).
 by apply/negP; rewrite -ltNge ltrBlDr ltrDl.
 Qed.
@@ -355,7 +355,7 @@ move: a => [b r|[|]] _ //.
     case: b => //; apply/contra_not/subset_has_ubound => x.
     by rewrite !set_itvE => /ltW.
   apply/has_ubPn => x; rewrite !set_itvE; exists (maxr (r + 1) (x + 1));
-  by rewrite ?in_itv /= ?andbT lt_maxr ltrDl ltr01 // orbT.
+  by rewrite ?in_itv /= ?andbT lt_max ltrDl ltr01 // orbT.
 case=> r /(_ (r + 1)) /=; rewrite in_itv /= => /(_ erefl).
 by apply/negP; rewrite -ltNge ltrDl.
 Qed.
diff --git a/theories/Rstruct.v b/theories/Rstruct.v
index 3ce44ea26..0ab9e873d 100644
--- a/theories/Rstruct.v
+++ b/theories/Rstruct.v
@@ -532,9 +532,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 /= le_maxr lexx.
+  by rewrite big_cons /= le_max lexx.
 rewrite ltnS => ti; case: t => [|h' t] // in IH ti *.
-by rewrite big_cons bigrmax_dflt le_maxr orbC IH.
+by rewrite big_cons bigrmax_dflt le_max orbC IH.
 Qed.
 
 (* Compatibilité avec l'addition *)
@@ -553,8 +553,8 @@ Proof.
 rewrite /bigmaxr; case: lr => // h t _.
 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 le_maxr lexx.
-- by rewrite lt_maxr ltxx => ?; rewrite max_r ?IH // ltW.
+- by rewrite le_max lexx.
+- by rewrite lt_max ltxx => ?; rewrite max_r ?IH // ltW.
 Qed.
 
 (* TODO: bigmaxr_morph? *)
diff --git a/theories/altreals/distr.v b/theories/altreals/distr.v
index b81cca9e7..d758964f7 100644
--- a/theories/altreals/distr.v
+++ b/theories/altreals/distr.v
@@ -81,10 +81,10 @@ Definition clamp (x : R) :=
   Num.max (Num.min x 1) 0.
 
 Lemma ge0_clamp x : 0 <= clamp x.
-Proof. by rewrite le_maxr lexx orbT. Qed.
+Proof. by rewrite le_max lexx orbT. Qed.
 
 Lemma le1_clamp x : clamp x <= 1.
-Proof. by rewrite le_maxl le_minl lexx ler01 orbT. Qed.
+Proof. by rewrite ge_max ge_min lexx ler01 orbT. Qed.
 
 Definition cp01_clamp := (ge0_clamp, le1_clamp).
 
@@ -1171,7 +1171,7 @@ 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 le_maxr lexx orbT.
+exists (Num.max M 0); first by rewrite le_max 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_wpM2r=> //; apply/ltW.
diff --git a/theories/altreals/realseq.v b/theories/altreals/realseq.v
index 7462ed1c7..54ee7789f 100644
--- a/theories/altreals/realseq.v
+++ b/theories/altreals/realseq.v
@@ -209,20 +209,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 lt_maxr ltr_wpDl.
+apply/asboolP/nboundedP; exists e => [|n]; first by rewrite lt_max ltr_wpDl.
 case: (ltnP n K); last first.
   move/cu; rewrite inE eclamp_id ?ltr01 // => ltunBx1.
-  rewrite lt_maxr; apply/orP; left; rewrite -[u n](addrK x) addrAC.
+  rewrite lt_max; apply/orP; left; rewrite -[u n](addrK x) addrAC.
   by apply/(le_lt_trans (ler_normD _ _)); rewrite addrC ltrD2l.
 move=> lt_nK; have: `|u n| \in S; first by apply/map_f; rewrite mem_iota.
-move=> un_S; rewrite lt_maxr; apply/orP; right.
+move=> un_S; rewrite lt_max; apply/orP; right.
 case E: {+}K lt_nK => [|k] // lt_nSk; apply/ltr_pwDr; 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 le_maxr lexx.
-by move/hux=> le_yux; rewrite le_maxr le_yux orbT.
+  by rewrite le_max lexx.
+by move/hux=> le_yux; rewrite le_max le_yux orbT.
 Qed.
 
 Lemma nboundedC c : nbounded c%:S.
diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v
index caaa40645..c5eac8ae6 100644
--- a/theories/altreals/realsum.v
+++ b/theories/altreals/realsum.v
@@ -107,14 +107,14 @@ Proof. by apply/normr_ge0. Qed.
 
 Lemma le_fpos_norm f x : fpos f x <= `|f x|.
 Proof.
-rewrite /fpos ger0_norm ?(le_maxr, lexx) //.
-by rewrite le_maxl normr_ge0 ler_norm.
+rewrite /fpos ger0_norm ?(le_max, lexx) //.
+by rewrite ge_max 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 ?le_maxr ?lexx //.
-by rewrite le_maxl lexx /=; case: ltP => //=; rewrite le_f.
+move=> le_f x; rewrite /fpos !ger0_norm ?le_max ?lexx //.
+by rewrite ge_max lexx /=; case: ltP => //=; rewrite le_f.
 Qed.
 
 Lemma fposBfneg f x : fpos f x - fneg f x = f x.
diff --git a/theories/charge.v b/theories/charge.v
index 6b98fac20..6c6fb76f5 100644
--- a/theories/charge.v
+++ b/theories/charge.v
@@ -623,7 +623,7 @@ Let nuA_g_ x : nu (A_ x) >= mine (g_ x * 2^-1%:E) 1.
 Proof. by move: x => [[[? ?] ?]] []. Qed.
 
 Let nuA_ge0 x : 0 <= nu (A_ x).
-Proof. by rewrite (le_trans _ (nuA_g_ _))// le_minr lee01 andbT mule_ge0. Qed.
+Proof. by rewrite (le_trans _ (nuA_g_ _))// le_min lee01 andbT mule_ge0. Qed.
 
 Let subDD A := [set nu E | E in [set E | measurable E /\ E `<=` D `\` A] ].
 
@@ -645,7 +645,7 @@ have /ereal_sup_gt/cid2[_ [B/= [mB BDA <- mnuB]]] : m < d_ A.
   rewrite /m; have [->|dn1oo] := eqVneq (d_ A) +oo.
     by rewrite min_r ?ltey ?gt0_mulye ?leey.
   rewrite -(@fineK _ (d_ A)); last by rewrite gt0_fin_numE// ltey.
-  rewrite -EFinM -fine_min// lte_fin lt_minl; apply/orP; left.
+  rewrite -EFinM -fine_min// lte_fin gt_min; apply/orP; left.
   by rewrite ltr_pdivrMr// ltr_pMr ?ltr1n// fine_gt0// d_gt0/= ltey.
 by exists B; split => //; rewrite (le_trans _ (ltW mnuB)).
 Qed.
@@ -699,7 +699,7 @@ have A_cvg_0 : nu (A_ (v n)) @[n --> \oo] --> 0.
 have mine_cvg_0 : (mine (g_ (v n) * 2^-1%:E) 1) @[n --> \oo] --> 0.
   apply: (@squeeze_cvge _ _ _ _ _ _ (fun n => nu (A_ (v n))));
     [|exact: cvg_cst|by []].
-  by apply: nearW => n /=; rewrite nuA_g_ andbT le_minr lee01 andbT mule_ge0.
+  by apply: nearW => n /=; rewrite nuA_g_ andbT le_min lee01 andbT mule_ge0.
 have g_cvg_0 : (g_ \o v) n @[n --> \oo] --> 0 by apply: mine2_cvg_0_cvg_0 => //=.
 have nuDAoo : nu D >= nu (D `\` Aoo).
   rewrite -[in leRHS](@setDUK _ Aoo D); last first.
@@ -780,7 +780,7 @@ have /ereal_inf_lt/cid2[_ [B/= [mB BU] <-] nuBm] : s_ U < m.
   rewrite /m; have [->|s0oo] := eqVneq (s_ U) -oo.
     by rewrite max_r ?ltNye// gt0_mulNye// leNye.
   rewrite -(@fineK _ (s_ U)); last by rewrite lt0_fin_numE// ltNye.
-  rewrite -EFinM -fine_max// lte_fin lt_maxr; apply/orP; left.
+  rewrite -EFinM -fine_max// lte_fin lt_max; apply/orP; left.
   by rewrite ltr_pdivlMr// gtr_nMr ?ltr1n// fine_lt0// s_lt0/= ltNye andbT.
 have [C [CB nsC nuCB]] := hahn_decomposition_lemma nu mB.
 exists C; split => //; first exact: (subset_trans CB).
@@ -818,7 +818,7 @@ have znuD n : z_ (v n) <= nu D.
   apply: (subset_trans DP); apply: subsetC; rewrite Ubig.
   exact: bigsetU_bigcup.
 have max_le0 n : maxe (z_ (v n) * 2^-1%:E) (- 1%E) <= 0.
-  by rewrite le_maxl leeN10 andbT pmule_lle0.
+  by rewrite ge_max leeN10 andbT pmule_lle0.
 have not_s_cvg_0 : ~ (z_ \o v) n @[n --> \oo]  --> 0.
   move/fine_cvgP => -[zfin] /cvgrPdist_lt.
   have /[swap] /[apply] -[M _ hM] : (0 < `|fine (nu D)|)%R.
@@ -849,7 +849,7 @@ have : cvg (series (fun n => fine (maxe (z_ (v n) * 2^-1%:E) (- 1%E))) n @[n -->
   rewrite (_ : _ \o _ = (fun n =>
     \sum_(0 <= k < n) fine (maxe (z_ (v k) * 2^-1%:E)%E (- 1%E)%E))%R) //.
   apply/funext => n/=; rewrite sum_fine// => m _.
-  rewrite le0_fin_numE; first by rewrite lt_maxr ltNyr orbT.
+  rewrite le0_fin_numE; first by rewrite lt_max ltNyr orbT.
   by rewrite /maxe; case: ifPn => // _; rewrite mule_le0_ge0.
 move/cvg_series_cvg_0 => maxe_cvg_0.
 apply: not_s_cvg_0.
@@ -864,13 +864,13 @@ apply/fine_cvgP; split.
     by apply: contra maxe_lt1 => /eqP ->; rewrite max_r ?leNye//= normrN1 lexx.
   by rewrite lt_eqF// (@le_lt_trans _ _ 0)// mule_le0_ge0.
 apply/cvgrPdist_lt => _ /posnumP[e].
-have : (0 < minr e%:num 1)%R by rewrite lt_minr// ltr01 andbT.
+have : (0 < minr e%:num 1)%R by rewrite lt_min// ltr01 andbT.
 move/cvgrPdist_lt : maxe_cvg_0 => /[apply] -[M _ hM].
 near=> n; rewrite sub0r normrN.
 have /hM : (M <= n)%N by near: n; exists M.
 rewrite sub0r normrN /maxe/=; case: ifPn => [_|].
-  by rewrite normrN normr1 lt_minr ltxx andbF.
-by rewrite -leNgt => ? /lt_le_trans; apply; rewrite le_minl lexx.
+  by rewrite normrN normr1 lt_min ltxx andbF.
+by rewrite -leNgt => ? /lt_le_trans; apply; rewrite ge_min lexx.
 Unshelve. all: by end_near. Qed.
 
 Lemma Hahn_decomposition_uniq P1 N1 P2 N2 :
diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v
index 13cc2fdc3..63adf6ecf 100644
--- a/theories/constructive_ereal.v
+++ b/theories/constructive_ereal.v
@@ -61,7 +61,7 @@ Require Import signed.
 (*             x%:nng == explicitly casts x to {nonneg \bar R}, in scope %E   *)
 (* ```                                                                        *)
 (*                                                                            *)
-(* ## Topology of extended real numbers                                        *)
+(* ## Topology of extended real numbers                                       *)
 (* ```                                                                        *)
 (*                       contract == order-preserving bijective function      *)
 (*                                   from extended real numbers to [-1; 1]    *)
@@ -1526,8 +1526,8 @@ split=> [-> // A A0|Ax]; first by rewrite leey.
 apply/eqP; rewrite eq_le leey /= leNgt; apply/negP.
 case: x Ax => [x Ax _|//|/(_ _ ltr01)//].
 suff: ~ x%:E < (Order.max 0 x + 1)%:E.
-  by apply; rewrite lte_fin ltr_pwDr// le_maxr lexx orbT.
-by apply/negP; rewrite -leNgt; apply/Ax/ltr_pwDr; rewrite // le_maxr lexx.
+  by apply; rewrite lte_fin ltr_pwDr// le_max lexx orbT.
+by apply/negP; rewrite -leNgt; apply/Ax/ltr_pwDr; rewrite // le_max lexx.
 Qed.
 
 #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `eqyP`")]
@@ -3534,39 +3534,55 @@ Local Notation nR := {compare (0 : \bar R) & nz & r}.
 Implicit Type x y : nR.
 Local Notation num := (@num _ _ (0 : R) nz r).
 
-Lemma num_lee_maxr a x y :
+Lemma num_lee_max a x y :
   a <= maxe x%:num y%:num = (a <= x%:num) || (a <= y%:num).
-Proof. by rewrite -comparable_le_maxr// ereal_comparable. Qed.
+Proof. by rewrite -comparable_le_max// ereal_comparable. Qed.
 
-Lemma num_lee_maxl a x y :
+Lemma num_gee_max a x y :
   maxe x%:num  y%:num <= a = (x%:num <= a) && (y%:num <= a).
-Proof. by rewrite -comparable_le_maxl// ereal_comparable. Qed.
+Proof. by rewrite -comparable_ge_max// ereal_comparable. Qed.
 
-Lemma num_lee_minr a x y :
+Lemma num_lee_min a x y :
   a <= mine x%:num y%:num = (a <= x%:num) && (a <= y%:num).
-Proof. by rewrite -comparable_le_minr// ereal_comparable. Qed.
+Proof. by rewrite -comparable_le_min// ereal_comparable. Qed.
 
-Lemma num_lee_minl a x y :
+Lemma num_gee_min a x y :
   mine x%:num y%:num <= a = (x%:num <= a) || (y%:num <= a).
-Proof. by rewrite -comparable_le_minl// ereal_comparable. Qed.
+Proof. by rewrite -comparable_ge_min// ereal_comparable. Qed.
 
-Lemma num_lte_maxr a x y :
+Lemma num_lte_max a x y :
   a < maxe x%:num y%:num = (a < x%:num) || (a < y%:num).
-Proof. by rewrite -comparable_lt_maxr// ereal_comparable. Qed.
+Proof. by rewrite -comparable_lt_max// ereal_comparable. Qed.
 
-Lemma num_lte_maxl a x y :
+Lemma num_gte_max a x y :
   maxe x%:num  y%:num < a = (x%:num < a) && (y%:num < a).
-Proof. by rewrite -comparable_lt_maxl// ereal_comparable. Qed.
+Proof. by rewrite -comparable_gt_max// ereal_comparable. Qed.
 
-Lemma num_lte_minr a x y :
+Lemma num_lte_min a x y :
   a < mine x%:num y%:num = (a < x%:num) && (a < y%:num).
-Proof. by rewrite -comparable_lt_minr// ereal_comparable. Qed.
+Proof. by rewrite -comparable_lt_min// ereal_comparable. Qed.
 
-Lemma num_lte_minl a x y :
+Lemma num_gte_min a x y :
   mine x%:num y%:num < a = (x%:num < a) || (y%:num < a).
-Proof. by rewrite -comparable_lt_minl// ereal_comparable. Qed.
+Proof. by rewrite -comparable_gt_min// ereal_comparable. Qed.
 
 End MorphReal.
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lee_max`")]
+Notation num_lee_maxr := num_lee_max (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gee_max`")]
+Notation num_lee_maxl := num_gee_max (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lee_min`")]
+Notation num_lee_minr := num_lee_min (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gee_min`")]
+Notation num_lee_minl := num_gee_min (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lte_max`")]
+Notation num_lte_maxr := num_lte_max (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gte_max`")]
+Notation num_lte_maxl := num_gte_max (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lte_min`")]
+Notation num_lte_minr := num_lte_min (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gte_min`")]
+Notation num_lte_minl := num_gte_min (only parsing).
 
 Section MorphGe0.
 Context {R : numDomainType} {nz : KnownSign.nullity}.
@@ -3796,8 +3812,8 @@ move=> [:wlog]; case: a b => [a||] [b||] //= ltax ltxb.
 - move: a b ltax ltxb; abstract: wlog. (*BUG*)
   move=> {}a {}b ltxa ltxb.
   have m_gt0 : (Num.min ((r - a) / 2) ((b - r) / 2) > 0)%R.
-    by rewrite lt_minr !divr_gt0 // ?subr_gt0.
-  exists (PosNum m_gt0) => y //=; rewrite lt_minr !ltr_distl.
+    by rewrite lt_min !divr_gt0 // ?subr_gt0.
+  exists (PosNum m_gt0) => y //=; rewrite lt_min !ltr_distl.
   move=> /andP[/andP[ay _] /andP[_ yb]].
   rewrite 2!lte_fin (lt_trans _ ay) ?(lt_trans yb) //=.
     rewrite -subr_gt0 opprD addrA {1}[(b - r)%R]splitr addrK.
diff --git a/theories/derive.v b/theories/derive.v
index 66ec8b403..312b96487 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -783,9 +783,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_pM ?pmulr_rge0 //; last by rewrite num_le_maxr /= lexx orbT.
+rewrite ler_pM ?pmulr_rge0 //; last by rewrite num_le_max /= lexx orbT.
 rewrite -ler_pdivlMl //.
-suff : `|x| <= k%:num ^-1 * e%:num by apply: le_trans; rewrite num_le_maxr /= lexx.
+suff : `|x| <= k%:num ^-1 * e%:num by apply: le_trans; rewrite num_le_max /= lexx.
 near: x; rewrite !near_simpl; apply/nbhs_le_nbhs_norm.
 by exists (k%:num ^-1 * e%:num) => //= ? /=; rewrite /= distrC subr0 => /ltW.
 Unshelve. all: by end_near. Qed.
@@ -849,7 +849,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 num_le_maxl /=.
+apply/eqoP => _/posnumP[e]; near=> x; rewrite num_ge_max /=.
 by apply/andP; split; near: x; apply: littleoP.
 Unshelve. all: by end_near. Qed.
 
diff --git a/theories/ereal.v b/theories/ereal.v
index da591ceb3..4d2fcce6f 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -5,7 +5,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 (* -------------------------------------------------------------------- *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect all_algebra finmap.
+From mathcomp Require Import all_ssreflect all_algebra finmap archimedean.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import fsbigop cardinality set_interval.
 Require Import reals signed topology.
@@ -686,7 +686,7 @@ case=> [x||].
     exists (Num.max (PosNum MP0) (PosNum MQ0))%:num.
     rewrite realE /= ge0 /=; split => //.
     case=> [r| |//].
-    * rewrite lte_fin/= num_max num_lt_maxl /= => /andP[MPx MQx]; split.
+    * rewrite lte_fin/= num_max num_gt_max /= => /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].
@@ -716,7 +716,7 @@ case=> [x||].
       exists (- (Num.max (PosNum MP0) (PosNum MQ0))%:num)%R.
       rewrite realN realE /= ge0 /=; split => //.
       case=> [r|//|].
-      - rewrite lte_fin ltrNr num_max num_lt_maxl => /andP[].
+      - rewrite lte_fin ltrNr num_max num_gt_max => /andP[].
         rewrite ltrNr => MPx; rewrite ltrNr => MQx; split.
           apply/ltMP; rewrite lte_fin (lt_le_trans MPx) //= lerNl -normrN.
           by rewrite real_ler_normr ?realN // lexx.
@@ -1204,7 +1204,7 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1].
       (r - fine (expand (contract r%:E - e%:num)))%R
       (fine (expand (contract r%:E + e%:num)) - r)%R.
     have e'0 : (0 < e')%R.
-      rewrite /e' lt_minr; apply/andP; split.
+      rewrite /e' lt_min; apply/andP; split.
         rewrite subr_gt0 -lte_fin -[in ltRHS](contractK r%:E).
         rewrite fine_expand // lt_expand// ?inE ?contract_le1 ?ltW//.
         by rewrite ltrBlDl ltrDr.
@@ -1213,8 +1213,8 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1].
     apply/nbhs_ballP; exists e' => // r' re'r'; apply reA.
     have [|r'r] := lerP r r'.
       move=> rr'; apply: ball_ereal_ball_fin_le => //.
-      by apply: le_ball re'r'; rewrite le_minl lexx orbT.
-    move: re'r'; rewrite /ball /= lt_minr => /andP[].
+      by apply: le_ball re'r'; rewrite ge_min lexx orbT.
+    move: re'r'; rewrite /ball /= lt_min => /andP[].
     rewrite gtr0_norm ?subr_gt0 // -ltrBlDl addrAC subrr add0r ltrNl.
     rewrite opprK -lte_fin fine_expand // => r'e'r _.
     exact: expand_ereal_ball_fin_lt.
@@ -1260,7 +1260,7 @@ rewrite predeq2E => x A; split.
                            (contract (r%:E + e%:num%:E) - contract r%:E)%R.
     exists (diag e'); rewrite /diag.
       exists e' => //.
-      rewrite /= /e' lt_minr; apply/andP; split.
+      rewrite /= /e' lt_min; apply/andP; split.
         by rewrite subr_gt0 lt_contract lte_fin ltrBlDr ltrDl.
       by rewrite subr_gt0 lt_contract lte_fin ltrDl.
     case=> [r' /= re'r'| |]/=.
@@ -1269,7 +1269,7 @@ rewrite predeq2E => x A; split.
         apply: reA; rewrite /ball /= real_ltr_norml // ?num_real //.
         rewrite ger0_norm ?subr_ge0// in re'r'.
         have : (contract (r%:E - e%:num%:E) < contract r'%:E)%R.
-          move: re'r'; rewrite /e' lt_minr => /andP[+ _].
+          move: re'r'; rewrite /e' lt_min => /andP[+ _].
           rewrite /e' ltrBrDl addrC -ltrBrDl => /lt_le_trans.
           by apply; rewrite opprB addrCA subrr addr0.
         rewrite -lt_expandRL ?inE ?contract_le1 // !contractK lte_fin.
@@ -1283,12 +1283,12 @@ rewrite predeq2E => x A; split.
       rewrite ltrNl opprB.
       rewrite /e' in re'r'.
       have r're : (contract r'%:E < contract (r%:E + e%:num%:E))%R.
-        move: re'r'; rewrite lt_minr => /andP[_].
+        move: re'r'; rewrite lt_min => /andP[_].
         by rewrite ltrBlDr subrK.
       rewrite ltrBlDr -lte_fin -(contractK (_ + r)%:E)%R.
       by rewrite addrC -(contractK r'%:E) // lt_expand ?inE ?contract_le1.
     * rewrite /ereal_ball [contract +oo]/=.
-      rewrite lt_minr => /andP[re'1 re'2].
+      rewrite lt_min => /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).
@@ -1303,7 +1303,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 lt_minr => /andP[re'1 _].
+      rewrite lt_min => /andP[re'1 _].
       move: re'1.
       rewrite ger0_norm; last first.
         rewrite addrC -lerBlDl add0r.
@@ -1402,21 +1402,21 @@ Lemma cvg_ereal_loc_seq (R : realType) (x : \bar R) :
 Proof.
 move=> P; rewrite /ereal_loc_seq.
 case: x => /= [x [_/posnumP[d] dP] |[d [dreal dP]] |[d [dreal dP]]]; last 2 first.
-    have /ZnatP [N Nfloor] : floor (Num.max d 0%R) \is a Znat.
-      by rewrite Znat_def floor_ge0 le_maxr lexx orbC.
+    have /ZnatP[N Nfloor] : floor (Num.max d 0%R) \is a Znat.
+      by rewrite Znat_def floor_ge0 le_max lexx orbC.
     exists N.+1 => // n ltNn; apply: dP; rewrite lte_fin.
-    have /le_lt_trans : (d <= Num.max d 0)%R by rewrite le_maxr lexx.
-    by apply; rewrite (lt_le_trans (lt_succ_floor _))// Nfloor natr1 ler_nat.
+    have /le_lt_trans : (d <= Num.max d 0)%R by rewrite le_max lexx.
+    by apply; rewrite (lt_le_trans (reals.lt_succ_floor _))// Nfloor natr1 ler_nat.
   have /ZnatP [N Nfloor] : floor (Num.max (- d)%R 0%R) \is a Znat.
-    by rewrite Znat_def floor_ge0 le_maxr lexx orbC.
+    by rewrite Znat_def floor_ge0 le_max lexx orbC.
   exists N.+1 => // n ltNn; apply: dP; rewrite lte_fin ltrNl.
-  have /le_lt_trans : (- d <= Num.max (- d) 0)%R by rewrite le_maxr lexx.
-  by apply; rewrite (lt_le_trans (lt_succ_floor _))// Nfloor natr1 ler_nat.
-have /ZnatP [N Nfloor] : floor (d%:num^-1) \is a Znat.
+  have /le_lt_trans : (- d <= Num.max (- d) 0)%R by rewrite le_max lexx.
+  by apply; rewrite (lt_le_trans (reals.lt_succ_floor _))// Nfloor natr1 ler_nat.
+have /ZnatP[N Nfloor] : floor (d%:num^-1) \is a Num.nat.
   by rewrite Znat_def floor_ge0.
 exists N => // n leNn; apply: dP; last first.
   by rewrite eq_sym addrC -subr_eq subrr eq_sym; exact/invr_neq0/lt0r_neq0.
 rewrite /= opprD addrA subrr distrC subr0 gtr0_norm; last by rewrite invr_gt0.
 rewrite -[ltLHS]mulr1 ltr_pdivrMl // -ltr_pdivrMr // div1r.
-by rewrite (lt_le_trans (lt_succ_floor _))// Nfloor lerD// ler_nat.
+by rewrite (lt_le_trans (reals.lt_succ_floor _))// Nfloor lerD// ler_nat.
 Qed.
diff --git a/theories/esum.v b/theories/esum.v
index 11232de2f..63250f50f 100644
--- a/theories/esum.v
+++ b/theories/esum.v
@@ -617,8 +617,8 @@ Proof.
 move=> Df Dg f0 g0.
 have /eqP : esum D (f \- g)^\+ + esum_posneg D g = esum D (f \- g)^\- + esum_posneg D f.
   rewrite !ge0_esum_posneg// -!esumD//; last 2 first.
-    by move=> t Dt; rewrite le_maxr lexx orbT.
-    by move=> t Dt; rewrite le_maxr lexx orbT.
+    by move=> t Dt; rewrite le_max lexx orbT.
+    by move=> t Dt; rewrite le_max lexx orbT.
   apply eq_esum => i Di; have [fg|fg] := leP 0 (f i - g i).
     rewrite max_r 1?leeNl ?oppe0// add0e subeK//.
     by rewrite fin_num_abs (summable_pinfty Dg).
diff --git a/theories/itv.v b/theories/itv.v
index e5ed3642c..b90c1580e 100644
--- a/theories/itv.v
+++ b/theories/itv.v
@@ -812,7 +812,7 @@ have [leuxlx|-> ->|lxneg uxneg|lxpos uxpos|lxneg uxpos] := interval_signP.
                                (Order.max (mulr (opp lx) (opp ly))
                                   (mulr ux uy))).
     rewrite /Itv.itv_cond itv_boundlr.
-    rewrite map_itv_bound_min map_itv_bound_max le_minl le_maxr.
+    rewrite map_itv_bound_min map_itv_bound_max ge_min le_max.
     rewrite -[x * y]opprK !opp_itv_boundl_subproof.
     rewrite -[in X in ((X || _) && _)]mulNr -[in X in ((_ || X) && _)]mulrN.
     rewrite -[in X in (_ && (X || _))]mulrNN !opprK.
diff --git a/theories/landau.v b/theories/landau.v
index c9fb5b13a..f3cf00dfc 100644
--- a/theories/landau.v
+++ b/theories/landau.v
@@ -482,7 +482,7 @@ split=> [[k k0 fOg] | [k [kreal fOg]]].
 exists (Num.max 1 `|k + 1|) => //.
 apply: fOg; rewrite (@lt_le_trans _ _ `|k + 1|) //.
   by rewrite (@lt_le_trans _ _ (k + 1)) ?ltrDl // real_ler_norm ?realD.
-by rewrite comparable_le_maxr ?real_comparable// lexx orbT.
+by rewrite comparable_le_max ?real_comparable// lexx orbT.
 Unshelve. end_near. Qed.
 
 Structure bigO_type (F : set_system T) (g : T -> W) := BigO {
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 2adb25c0e..488b4b005 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -1,8 +1,9 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
+From mathcomp Require Import archimedean.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import cardinality fsbigop .
+From mathcomp Require Import cardinality fsbigop.
 Require Import signed reals ereal topology normedtype sequences real_interval.
 Require Import esum measure lebesgue_measure numfun realfun function_spaces.
 
@@ -1282,22 +1283,22 @@ Lemma bigsetU_dyadic_itv n : `[n%:R, n.+1%:R[%classic =
   \big[setU/set0]_(n * 2 ^ n.+1 <= k < n.+1 * 2 ^ n.+1) [set` I n.+1 k].
 Proof.
 rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|].
-- rewrite -bigcup_seq /=; exists `|floor (r * 2 ^+ n.+1)|%N.
+- rewrite -bigcup_seq /=; exists `|reals.floor (r * 2 ^+ n.+1)|%N.
     rewrite /= mem_index_iota; apply/andP; split.
-      rewrite -ltez_nat gez0_abs ?floor_ge0; last first.
+      rewrite -ltez_nat gez0_abs ?reals.floor_ge0; last first.
         by rewrite mulr_ge0// (le_trans _ nr).
-      apply: (@le_trans _ _ (floor (n * 2 ^ n.+1)%:R)); last first.
+      apply: (@le_trans _ _ (reals.floor (n * 2 ^ n.+1)%:R)); last first.
         by apply: le_floor; rewrite natrM natrX ler_pM2r.
       by rewrite floor_natz intz.
     rewrite -ltz_nat gez0_abs; last first.
       by rewrite floor_ge0 mulr_ge0// (le_trans _ nr).
-    rewrite -(@ltr_int R) (le_lt_trans (floor_le _))//.
+    rewrite -(@ltr_int R) (le_lt_trans (reals.floor_le _))//.
     by rewrite PoszM intrM -natrX ltr_pM2r.
   rewrite /= in_itv /=; apply/andP; split.
-    rewrite ler_pdivrMr// (le_trans _ (floor_le _))//.
-    by rewrite -(@gez0_abs (floor _))// floor_ge0 mulr_ge0// (le_trans _ nr).
-  rewrite ltr_pdivlMr// (lt_le_trans (lt_succ_floor _))//.
-  rewrite -[in leRHS]natr1 lerD2r// -(@gez0_abs (floor _))// floor_ge0.
+    rewrite ler_pdivrMr// (le_trans _ (reals.floor_le _))//.
+    by rewrite -(@gez0_abs (reals.floor _))// floor_ge0 mulr_ge0// (le_trans _ nr).
+  rewrite ltr_pdivlMr// (lt_le_trans (reals.lt_succ_floor _))//.
+  rewrite -[in leRHS]natr1 lerD2r// -(@gez0_abs (reals.floor _))// floor_ge0.
   by rewrite mulr_ge0// (le_trans _ nr).
 - rewrite -bigcup_seq => -[/= k] /[!mem_index_iota] /andP[nk kn].
   rewrite in_itv /= => /andP[knr rkn]; rewrite in_itv /=; apply/andP; split.
@@ -1425,18 +1426,18 @@ rewrite pnatr_eq0 => /eqP.
 have [//|] := boolP (x \in B n).
 rewrite notin_setE /B /setI /= => /not_andP[] // /negP.
 rewrite -ltNge => fxn _.
-have K : (`|floor (fine (f x) * 2 ^+ n)| < n * 2 ^ n)%N.
-  rewrite -ltz_nat gez0_abs; last by rewrite floor_ge0 mulr_ge0// ltW.
-  rewrite -(@ltr_int R); rewrite (le_lt_trans (floor_le _))// PoszM intrM.
+have K : (`|reals.floor (fine (f x) * 2 ^+ n)| < n * 2 ^ n)%N.
+  rewrite -ltz_nat gez0_abs; last by rewrite reals.floor_ge0 mulr_ge0// ltW.
+  rewrite -(@ltr_int R); rewrite (le_lt_trans (reals.floor_le _))// PoszM intrM.
   by rewrite -natrX ltr_pM2r// -lte_fin (fineK fxfin).
 have /[!mem_index_enum]/(_ isT) := An0 (Ordinal K).
 rewrite implyTb indicE mem_set ?mulr1; last first.
   rewrite /A K /= inE; split=> //=; exists (fine (f x)); last by rewrite fineK.
   rewrite in_itv /=; apply/andP; split.
-    rewrite ler_pdivrMr// (le_trans _ (floor_le _))//.
-    by rewrite -(@gez0_abs (floor _))// floor_ge0 mulr_ge0// ltW.
-  rewrite ltr_pdivlMr// (lt_le_trans (lt_succ_floor _))// -[in leRHS]natr1.
-  by rewrite lerD2r// -{1}(@gez0_abs (floor _))// floor_ge0// mulr_ge0// ltW.
+    rewrite ler_pdivrMr// (le_trans _ (reals.floor_le _))//.
+    by rewrite -(@gez0_abs (reals.floor _))// reals.floor_ge0 mulr_ge0// ltW.
+  rewrite ltr_pdivlMr// (lt_le_trans (reals.lt_succ_floor _))// -[in leRHS]natr1.
+  by rewrite lerD2r// -{1}(@gez0_abs (reals.floor _))// reals.floor_ge0// mulr_ge0// ltW.
 rewrite mulf_eq0// -exprVn; apply/negP; rewrite negb_or expf_neq0//= andbT.
 rewrite pnatr_eq0 -lt0n absz_gt0 floor_neq0// -ler_pdivrMr//.
 apply/orP; right; apply/ltW; near: n.
@@ -1533,11 +1534,11 @@ near=> n.
 have mn : (m <= n)%N by near: n; exists m.
 have : fine (f x) < n%:R.
   near: n.
-  exists `|floor (fine (f x))|.+1%N => //= p /=.
+  exists `|reals.floor (fine (f x))|.+1%N => //= p /=.
   rewrite -(@ler_nat R); apply: lt_le_trans.
-  rewrite -natr1 (_ : `| _ |%:R  = (floor (fine (f x)))%:~R); last first.
-    by rewrite -[in RHS](@gez0_abs (floor _))// floor_ge0//; exact/fine_ge0/f0.
-  by rewrite lt_succ_floor.
+  rewrite -natr1 (_ : `| _ |%:R  = (reals.floor (fine (f x)))%:~R); last first.
+    by rewrite -[in RHS](@gez0_abs (reals.floor _))// reals.floor_ge0//; exact/fine_ge0/f0.
+  by rewrite reals.lt_succ_floor.
 rewrite -lte_fin (fineK fxfin) => fxn.
 have [approx_nx0|[k [/andP[k0 kn2n] ? ->]]] := f_ub_approx fxn.
   by have := Hm _ mn; rewrite approx_nx0.
@@ -1573,21 +1574,21 @@ move=> Dx fxoo; have approx_x n : approx n x = n%:R.
   by rewrite fgen_A0 // ?mulr0 // fxoo leey.
 case/cvg_ex => /= l; have [l0|l0] := leP 0%R l.
 - move=> /cvgrPdist_lt/(_ _ ltr01) -[n _].
-  move=> /(_ (`|ceil l|.+1 + n)%N) /= /(_ (leq_addl _ _)).
+  move=> /(_ (`|reals.ceil l|.+1 + n)%N) /= /(_ (leq_addl _ _)).
   rewrite approx_x.
   apply/negP; rewrite -leNgt distrC (le_trans _ (lerB_normD _ _)) //.
   rewrite normrN lerBrDl addSnnS [leRHS]ger0_norm ?ler0n//.
   rewrite natrD lerD// ?ler1n// ger0_norm // (le_trans (ceil_ge _)) //.
-  by rewrite -(@gez0_abs (ceil _)) // ceil_ge0.
+  by rewrite -(@gez0_abs (reals.ceil _)) // ceil_ge0.
 - move/cvgrPdist_lt => /(_ _ ltr01) -[n _].
-  move=> /(_ (`|floor l|.+1 + n)%N) /= /(_ (leq_addl _ _)).
+  move=> /(_ (`|reals.floor l|.+1 + n)%N) /= /(_ (leq_addl _ _)).
   rewrite approx_x.
   apply/negP; rewrite -leNgt distrC (le_trans _ (lerB_normD _ _)) //.
   rewrite normrN lerBrDl addSnnS [leRHS]ger0_norm ?ler0n//.
   rewrite natrD lerD// ?ler1n// ler0_norm //; last by rewrite ltW.
-  rewrite (@le_trans _ _ (- floor l)%:~R) //.
-    by rewrite mulrNz lerNl opprK floor_le.
-  by rewrite -(@lez0_abs (floor _)) // floor_le0 // ltW.
+  rewrite (@le_trans _ _ (- reals.floor l)%:~R) //.
+    by rewrite mulrNz lerNl opprK reals.floor_le.
+  by rewrite -(@lez0_abs (reals.floor _)) // reals.floor_le0 // ltW.
 Qed.
 
 Lemma ecvg_approx (f0 : forall x, D x -> (0 <= f x)%E) x :
@@ -2169,7 +2170,7 @@ apply/nondecreasing_seqP => n; apply/lefP => x; rewrite 2!bigmax_nnsfunE.
 rewrite (@le_trans _ _ (\big[maxr/0]_(i < n) g2 i n.+1 x)%R) //.
   apply: le_bigmax2 => i _; apply: (nondecreasing_seqP (g2 i ^~ x)).2 => a b ab.
    by rewrite !nnsfun_approxE; exact/lefP/nd_approx.
-rewrite (bigmaxD1 ord_max)// le_maxr; apply/orP; right.
+rewrite (bigmaxD1 ord_max)// le_max; apply/orP; right.
 rewrite [leRHS](eq_bigl (fun i => nat_of_ord i < n)%N).
   by rewrite (big_ord_narrow (leqnSn n)).
 move=> i /=; rewrite neq_lt; apply/orP/idP => [[//|]|]; last by left.
@@ -2327,7 +2328,7 @@ transitivity (\int[mu]_(x in D) limn (g^~ x)).
       exists 1%N => // m /= m0.
       by rewrite mulry gtr0_sg// ?mul1e ?leey// ltr0n.
     near=> n; rewrite lee_fin -ler_pdivrMr//.
-    near: n; exists `|ceil (M / r)|%N => // m /=.
+    near: n; exists `|reals.ceil (M / r)|%N => // m /=.
     rewrite -(ler_nat R); apply: le_trans.
     by rewrite natr_absz ger0_norm ?ceil_ge// ceil_ge0// divr_ge0// ?ltW.
   - rewrite lt0_mulye//; apply/cvgeNyPleNy; near=> M;
@@ -2336,7 +2337,7 @@ transitivity (\int[mu]_(x in D) limn (g^~ x)).
       exists 1%N => // m /= m0.
       by rewrite mulrNy gtr0_sg// ?ltr0n// mul1e ?leNye.
     near=> n; rewrite lee_fin -ler_ndivrMr//.
-    near: n; exists `|ceil (M / r)|%N => // m /=.
+    near: n; exists `|reals.ceil (M / r)|%N => // m /=.
     rewrite -(ler_nat R); apply: le_trans.
     rewrite natr_absz ger0_norm ?ceil_ge// ceil_ge0// -mulrNN.
     by rewrite mulr_ge0// lerNr oppr0// ltW// invr_lt0.
@@ -2358,7 +2359,7 @@ rewrite -(@fineK _ (\int[mu]_(x in D) f x)); last first.
 rewrite -lee_pdivr_mulr//; last first.
   by move: if_gt0 ifoo; case: (\int[mu]_(x in D) f x).
 near: n.
-exists `|ceil (M * (fine (\int[mu]_(x in D) f x))^-1)|%N => //.
+exists `|reals.ceil (M * (fine (\int[mu]_(x in D) f x))^-1)|%N => //.
 move=> n /=; rewrite -(@ler_nat R) -lee_fin; apply: le_trans.
 rewrite lee_fin natr_absz ger0_norm ?ceil_ge// ceil_ge0//.
 by rewrite mulr_ge0// ?invr_ge0//; exact/fine_ge0/integral_ge0.
@@ -2589,7 +2590,7 @@ Proof.
 move=> muD0; pose g : (T -> \bar R)^nat := fun n => cst n%:R%:E.
 have <- : (fun t => limn (g^~ t)) = cst +oo.
   rewrite funeqE => t; apply/cvg_lim => //=.
-  apply/cvgeryP/cvgryPge => M; exists `|ceil M|%N => //= m.
+  apply/cvgeryP/cvgryPge => M; exists `|reals.ceil M|%N => //= m.
   rewrite /= -(ler_nat R); apply: le_trans.
   by rewrite (le_trans (ceil_ge _))// natr_absz ler_int ler_norm.
 rewrite monotone_convergence //.
@@ -2598,7 +2599,7 @@ rewrite monotone_convergence //.
   have [muDoo|muDoo] := ltP (mu D) +oo; last first.
     exists 1%N => // m /= m0; move: muDoo; rewrite leye_eq => /eqP ->.
     by rewrite mulry gtr0_sg ?mul1e ?leey// ltr0n.
-  exists `|ceil (M / fine (mu D))|%N => // m /=.
+  exists `|reals.ceil (M / fine (mu D))|%N => // m /=.
   rewrite -(ler_nat R) => MDm; rewrite -(@fineK _ (mu D)) ?ge0_fin_numE//.
   rewrite -lee_pdivr_mulr; last by rewrite fine_gt0// lt0e muD0 measure_ge0.
   rewrite lee_fin (le_trans _ MDm)//.
@@ -3421,7 +3422,7 @@ have [M M0 muM] : exists2 M, (0 <= M)%R &
 apply/eqP/negPn/negP => /eqP muED0; move/not_forallP : muM; apply.
 have [muEDoo|] := ltP (mu (E `&` D)) +oo; last first.
   by rewrite leye_eq => /eqP ->; exists 1%N; rewrite mul1e leye_eq.
-exists `|ceil (M * (fine (mu (E `&` D)))^-1)|%N.+1.
+exists `|reals.ceil (M * (fine (mu (E `&` D)))^-1)|%N.+1.
 apply/negP; rewrite -ltNge.
 rewrite -[X in _ * X](@fineK _ (mu (E `&` D))); last first.
   by rewrite fin_numElt muEDoo (lt_le_trans _ (measure_ge0 _ _)).
@@ -3669,7 +3670,7 @@ move=> mf; split=> [iDf0|Df0].
     rewrite predeqE => t; split=> [[Dt ft0]|[n _ /= [Dt nft]]].
       have [ftoo|ftoo] := eqVneq `|f t| +oo.
         by exists 0%N => //; split => //=; rewrite ftoo /= leey.
-      pose m := `|ceil (fine `|f t|)^-1|%N.
+      pose m := `|reals.ceil (fine `|f t|)^-1|%N.
       have ftfin : `|f t|%E \is a fin_num by rewrite ge0_fin_numE// ltey.
       exists m => //; split => //=.
       rewrite -(@fineK _ `|f t|) // lee_fin -ler_pV2; last 2 first.
@@ -4121,7 +4122,7 @@ move=> sa.
 transitivity (\int[mseries (fun n => [the measure _ _ of \d_ n]) O]_t a t).
   congr (integral _ _ _); apply/funext => A.
   by rewrite /= counting_dirac.
-rewrite (@ge0_integral_measure_series _ _ R (fun n => [the measure _ _ of \d_ n]) setT)//=.
+rewrite (@ge0_integral_measure_series _ _ R (fun n => \d_ n) setT)//=.
 by apply: eq_eseriesr=> i _; rewrite integral_dirac//= diracT mul1e.
 Qed.
 
@@ -6440,7 +6441,7 @@ move=> Ef; have {Ef} : mu.-negligible (E `&` [set x | 0 < f^* x]).
   near \oo => m; exists m => //=.
   rewrite -(@fineK _ (f^* x)) ?gt0_fin_numE ?ltey// lte_fin.
   rewrite invf_plt ?posrE//; last by rewrite fine_gt0// ltey fx0.
-  set r := _^-1; rewrite (@le_lt_trans _ _ `|ceil r|.+1%:R)//.
+  set r := _^-1; rewrite (@le_lt_trans _ _ `|reals.ceil r|.+1%:R)//.
     by rewrite (le_trans _ (abs_ceil_ge _))// ler_norm.
   by rewrite ltr_nat ltnS; near: m; exact: nbhs_infty_gt.
 apply: negligibleS => z /= /not_implyP[Ez H]; split => //.
@@ -6642,14 +6643,14 @@ have fE y k r : (ball 0%R k.+1%:R) y -> (r < 1)%R ->
   rewrite (le_trans (ltW yk1))// -lerBlDr opprK -lerBrDl.
   rewrite -natrB//; last by rewrite -addnn addSnnS ltn_addl.
   by rewrite -addnn addnK ler1n.
-have := h `|ceil x|.+1%N Logic.I.
-have Bxx : B `|ceil x|.+1 x.
+have := h `|reals.ceil x|.+1%N Logic.I.
+have Bxx : B `|reals.ceil x|.+1 x.
   rewrite /B /ball/= sub0r normrN (le_lt_trans (abs_ceil_ge _))// ltr_nat.
   by rewrite -addnn addSnnS ltn_addl.
 move=> /(_ Bxx)/fine_cvgP[davg_fk_fin_num davg_fk0].
 have f_fk_ceil : \forall t \near 0^'+,
   \int[mu]_(y in ball x t) `|(f y)%:E - (f x)%:E| =
-  \int[mu]_(y in ball x t) `|fk `|ceil x|.+1 y - fk `|ceil x|.+1 x|%:E.
+  \int[mu]_(y in ball x t) `|fk `|reals.ceil x|.+1 y - fk `|reals.ceil x|.+1 x|%:E.
   near=> t.
   apply: eq_integral => /= y /[1!inE] xty.
   rewrite -(fE x _ t)//; last first.
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index 16499b529..77545aecb 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -1800,9 +1800,9 @@ move=> mf mg mD; apply: (measurability (ErealGenCInfty.measurableE R)) => //.
 move=> _ [_ [x ->] <-]; rewrite [X in measurable X](_ : _ =
     (D `&` f @^-1` `[x%:E, +oo[) `|` (D `&` g @^-1` `[x%:E, +oo[)); last first.
   rewrite predeqE => t /=; split.
-    by rewrite !/= /= !in_itv /= !andbT le_maxr => -[Dx /orP[|]];
+    by rewrite !/= /= !in_itv /= !andbT le_max => -[Dx /orP[|]];
       tauto.
-  by move=> [|]; rewrite !/= /= !in_itv/= !andbT le_maxr;
+  by move=> [|]; rewrite !/= /= !in_itv/= !andbT le_max;
     move=> [Dx ->]//; rewrite orbT.
 by apply: measurableU; [exact/mf/emeasurable_itv| exact/mg/emeasurable_itv].
 Qed.
@@ -2176,12 +2176,12 @@ wlog VB1 : V ABV / forall i, V i -> ((radius (B i))%:num <= 1)%R.
   pose V' := V `\` [set i | (radius (B i))%:num > 1]%R.
   have : vitali_cover A B V'.
     split; [exact: ABV.1|move=> x Ax e e0].
-    have : (0 < minr e 1)%R by rewrite lt_minr// e0/=.
+    have : (0 < minr e 1)%R by rewrite lt_min// e0/=.
     move=> /(ABV.2 x Ax)[i [Vi ix ie]].
     exists i; split => //.
     - split => //=; rewrite ltNge; apply/negP/negPn.
-      by rewrite (le_trans (ltW ie))// le_minl lexx orbT.
-    - by rewrite (lt_le_trans ie)// le_minl lexx.
+      by rewrite (le_trans (ltW ie))// ge_min lexx orbT.
+    - by rewrite (lt_le_trans ie)// ge_min lexx.
   move/wlg.
   have V'B1 i : V' i -> ((radius (B i))%:num <= 1)%R.
     by move=> [Vi /=]; rewrite ltNge => /negP/negPn.
@@ -2344,11 +2344,11 @@ have ZNF5 : Z r%:num `<=`
         (d%:num < r%:num - `|z|)%R & closed_ball z d%:num `&` K = set0.
       have [d/= d0 dzK] := closed_disjoint_closed_ball closedK Kz.
       have rz0 : (0 < minr ((r%:num - `|z|) / 2) (d / 2))%R.
-        by rewrite lt_minr (divr_gt0 d0)//= andbT divr_gt0// subr_gt0.
+        by rewrite lt_min (divr_gt0 d0)//= andbT divr_gt0// subr_gt0.
       exists (PosNum rz0) => /=.
-        by rewrite lt_minl ltr_pdivrMr// ltr_pMr ?subr_gt0// ltr1n.
+        by rewrite gt_min ltr_pdivrMr// ltr_pMr ?subr_gt0// ltr1n.
       apply: dzK => //=.
-      rewrite sub0r normrN gtr0_norm// lt_minl (ltr_pdivrMr d d)//.
+      rewrite sub0r normrN gtr0_norm// gt_min (ltr_pdivrMr d d)//.
       by rewrite ltr_pMr// ltr1n orbT.
     have N0_gt0 : (0 < d%:num / 2)%R by rewrite divr_gt0.
     have [i [Vi Biz BiN0]] := ABV _ Az _ N0_gt0.
diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v
index 656c51fff..e5978362a 100644
--- a/theories/lebesgue_stieltjes_measure.v
+++ b/theories/lebesgue_stieltjes_measure.v
@@ -129,7 +129,7 @@ rewrite /Order.meet/= /Order.meet/= /Order.join/=
          ?(andbF, orbF)/= ?(meetEtotal, joinEtotal).
 rewrite -negb_or le_total/=; set c := minr _ _; set d := maxr _ _.
 have inside : a.1 < c -> d < a.2 -> `]a.1, c] `&` `]d, a.2] = set0.
-  rewrite -subset0 lt_minr lt_maxl => /andP[a12 ab1] /andP[_ ba2] x /= [].
+  rewrite -subset0 lt_min gt_max => /andP[a12 ab1] /andP[_ ba2] x /= [].
   have b1a2 : b.1 <= a.2 by rewrite ltW// (lt_trans ltb).
   have a1b2 : a.1 <= b.2 by rewrite ltW// (lt_trans _ ltb).
   rewrite /c /d (min_idPr _)// (max_idPr _)// !in_itv /=.
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 34c308c41..365b3c9fa 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -3,6 +3,7 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix.
 From mathcomp Require Import rat interval zmodp vector fieldext falgebra.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import archimedean.
 From mathcomp Require Import cardinality set_interval Rstruct.
 Require Import ereal reals signed topology prodnormedzmodule function_spaces.
 
@@ -251,10 +252,10 @@ End pseudoMetricnormedzmodule_lemmas.
 Lemma bigcup_ballT {R : realType} : \bigcup_n ball (0%R : R) n%:R = setT.
 Proof.
 apply/seteqP; split => // x _; have [x0|x0] := ltP 0%R x.
-  exists `|ceil x|.+1 => //.
+  exists `|reals.ceil x|.+1 => //.
   rewrite /ball /= sub0r normrN gtr0_norm// (le_lt_trans (ceil_ge _))//.
   by rewrite -natr1 natr_absz -abszE gtz0_abs// ?ceil_gt0// ltr_pwDr.
-exists `|ceil (- x)|.+1 => //.
+exists `|reals.ceil (- x)|.+1 => //.
 rewrite /ball /= sub0r normrN ler0_norm// (le_lt_trans (ceil_ge _))//.
 rewrite -natr1 natr_absz -abszE gez0_abs ?ceil_ge0// 1?lerNr ?oppr0//.
 by rewrite ltr_pwDr.
@@ -367,7 +368,7 @@ apply Build_ProperFilter.
 split=> /= [|P Q [MP [MPr gtMP]] [MQ [MQr gtMQ]] |P Q sPQ [M [Mr gtM]]].
 - by exists 0.
 - exists (maxr MP MQ); split=> [|x]; first exact: max_real.
-  by rewrite comparable_lt_maxl ?real_comparable // => /andP[/gtMP ? /gtMQ].
+  by rewrite comparable_gt_max ?real_comparable // => /andP[/gtMP ? /gtMQ].
 - by exists M; split => // ? /gtM /sPQ.
 Qed.
 
@@ -379,7 +380,7 @@ apply Build_ProperFilter.
 split=> /= [|P Q [MP [MPr ltMP]] [MQ [MQr ltMQ]] |P Q sPQ [M [Mr ltM]]].
 - by exists 0.
 - exists (Num.min MP MQ); split=> [|x]; first exact: min_real.
-  by rewrite comparable_lt_minr ?real_comparable // => /andP[/ltMP ? /ltMQ].
+  by rewrite comparable_lt_min ?real_comparable // => /andP[/ltMP ? /ltMQ].
 - by exists M; split => // x /ltM /sPQ.
 Qed.
 
@@ -595,7 +596,7 @@ Proof.
 split=> [/cvgryPge|/cvgnyPge] Foo.
   by apply/cvgnyPge => A; near do rewrite -(@ler_nat R); apply: Foo.
 apply/cvgryPgey; near=> A; near=> n.
-rewrite (le_trans (@ceil_ge R A))// (ler_int _ _ (f n)) [ceil _]intEsign.
+rewrite (le_trans (@ceil_ge R A))// (ler_int _ _ (f n)) [reals.ceil _]intEsign.
 by rewrite le_gtF ?expr0 ?mul1r ?lez_nat ?ceil_ge0//; near: n; apply: Foo.
 Unshelve. all: by end_near. Qed.
 
@@ -2281,7 +2282,7 @@ 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 comparable_lt_maxl// ?real_comparable//; split=> /andP.
+by rewrite comparable_gt_max// ?real_comparable//; split=> /andP.
 Qed.
 
 Lemma prod_norm_ball :
@@ -3409,7 +3410,7 @@ pose f z := (f' z)/eps%:num; exists f; split.
   apply: fine_cvg; first exact: nbhs_filter.
   rewrite fineK //; first exact: edist_inf_continuous.
 - move=> _ [x _ <-]; rewrite set_itvE /=; apply/andP; split.
-    by rewrite /f divr_ge0 // /f' /= le_minr fine_ge0//= edist_inf_ge0.
+    by rewrite /f divr_ge0 // /f' /= le_min fine_ge0//= edist_inf_ge0.
   by rewrite /f ler_pdivrMr // mul1r /f' /= /minr; case: ltP => // /ltW.
 - by move=> ? [z Az] <-; rewrite /f/f' /= edist_inf0 // /minr fine0 ifT ?mul0r.
 - move=> ? [b Bb] <-; rewrite /f /f'/= /minr/=.
@@ -4918,7 +4919,7 @@ Lemma compact_bounded (K : realType) (V : normedModType K) (A : set V) :
 Proof.
 rewrite compact_cover => Aco.
 have covA : A `<=` \bigcup_(n : int) [set p | `|p| < n%:~R].
-  by move=> p _; exists (floor `|p| + 1) => //; rewrite rmorphD/= lt_succ_floor.
+  by move=> p _; exists (reals.floor `|p| + 1) => //; rewrite rmorphD/= reals.lt_succ_floor.
 have /Aco [] := covA.
   move=> n _; rewrite openE => p; rewrite /= -subr_gt0 => ltpn.
   apply/nbhs_ballP; exists (n%:~R - `|p|) => // q.
@@ -5519,9 +5520,9 @@ move=> {}xy; have [rs|sr] := ltP r s.
     by apply; rewrite xrys /ball/= ltr_distlC !ltrD2l -ltr_norml gtr0_norm.
   by rewrite /ball/= ltr_distlC ltrD2r (ltNge y) (ltW xy) andbF.
 - suff : ~ ball y s (x - r + minr ((y - x) / 2) r).
-    apply; rewrite -xrys /ball/= ltr_distlC ltrDl lt_minr r0 andbT.
+    apply; rewrite -xrys /ball/= ltr_distlC ltrDl lt_min r0 andbT.
     rewrite divr_gt0 ?subr_gt0//= addrAC ltrBlDl addrCA ler_ltD//.
-    by rewrite lt_minl ltrDl r0 orbT.
+    by rewrite gt_min ltrDl r0 orbT.
   have [yx2r|ryx2] := ltP ((y - x) / 2) r.
     rewrite /ball/= ltr_distlC => /andP[+ _]; rewrite -(@ltr_pM2l _ 2)//.
     rewrite !mulrDr mulrCA divff// mulr1 ltNge => /negP; apply.
@@ -5762,13 +5763,13 @@ Notation r_gt0 := vitali_collection_partition_ub_gt0.
 Lemma ex_vitali_collection_partition i :
   V i -> exists n, vitali_collection_partition n i.
 Proof.
-move=> Vi; pose f := floor (r / (radius (B i))%:num).
+move=> Vi; pose f := reals.floor (r / (radius (B i))%:num).
 have f_ge0 : 0 <= f by rewrite floor_ge0// divr_ge0// ltW// (r_gt0 Vi).
 have [m /andP[mf fm]] := leq_ltn_expn `|f|.-1.
 exists m; split => //; apply/andP; split => [{mf}|{fm}].
   rewrite -(@ler_nat R) in fm.
   rewrite ltr_pdivrMr// mulrC -ltr_pdivrMr// (lt_le_trans _ fm)//.
-  rewrite (lt_le_trans (lt_succ_floor _))//= -/f -natr1 lerD2r//.
+  rewrite (lt_le_trans (reals.lt_succ_floor _))//= -/f -natr1 lerD2r//.
   have [<-|f0] := eqVneq 0 f; first by rewrite /= ler0n.
   rewrite prednK//; last by rewrite absz_gt0 eq_sym.
   by rewrite natr_absz// ger0_norm.
@@ -5778,7 +5779,7 @@ rewrite ler_pdivlMr// mulrC -ler_pdivlMr//.
 have [f0|f0] := eqVneq 0 f.
   by move: mf; rewrite -f0 absz0 leNgt expnS ltr_nat leq_pmulr// expn_gt0.
 rewrite (le_trans mf)// prednK//; last by rewrite absz_gt0 eq_sym.
-by rewrite natr_absz// ger0_norm// floor_le.
+by rewrite natr_absz// ger0_norm// reals.floor_le.
 Qed.
 
 Lemma cover_vitali_collection_partition :
@@ -5972,7 +5973,7 @@ Qed.
 
 Lemma vitali_lemma_infinite_cover : { D : set I | [/\ countable D,
   D `<=` V, trivIset D (closure\o B) &
-  cover V (closure\o B) `<=` cover D (closure \o scale_ball 5%:R \o B)] }.
+  cover V (closure \o B) `<=` cover D (closure \o scale_ball 5%:R \o B)] }.
 Proof.
 have [D [cD DV tD maxD]] := vitali_lemma_infinite.
 exists D; split => // x [i Vi] cBix/=.
diff --git a/theories/numfun.v b/theories/numfun.v
index 888641c90..2415c34cd 100644
--- a/theories/numfun.v
+++ b/theories/numfun.v
@@ -140,10 +140,10 @@ Variables (T : Type) (R : realDomainType) (D : set T).
 Implicit Types (f g : T -> \bar R) (r : R).
 
 Lemma funepos_ge0 f x : 0 <= f^\+ x.
-Proof. by rewrite /funepos /= le_maxr lexx orbT. Qed.
+Proof. by rewrite /funepos /= le_max lexx orbT. Qed.
 
 Lemma funeneg_ge0 f x : 0 <= f^\- x.
-Proof. by rewrite /funeneg le_maxr lexx orbT. Qed.
+Proof. by rewrite /funeneg le_max lexx orbT. Qed.
 
 Lemma funeposN f : (\- f)^\+ = f^\-. Proof. exact/funext. Qed.
 
diff --git a/theories/prodnormedzmodule.v b/theories/prodnormedzmodule.v
index 199cdf769..fcdfff5da 100644
--- a/theories/prodnormedzmodule.v
+++ b/theories/prodnormedzmodule.v
@@ -1,3 +1,4 @@
+(* mathcomp analysis (c) 2020 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect fingroup ssralg poly ssrnum.
 Require Import signed.
@@ -24,13 +25,13 @@ 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 num_le_maxl !(le_trans (ler_normD _ _)) ?lerD//;
-by rewrite comparable_le_maxr ?lexx ?orbT// real_comparable.
+rewrite /norm num_ge_max !(le_trans (ler_normD _ _)) ?lerD//;
+by rewrite comparable_le_max ?lexx ?orbT// real_comparable.
 Qed.
 
 Lemma norm_eq0 x : norm x = 0 -> x = 0.
 Proof.
-case: x => x1 x2 /eqP; rewrite eq_le num_le_maxl 2!normr_le0 -andbA/=.
+case: x => x1 x2 /eqP; rewrite eq_le num_ge_max 2!normr_le0 -andbA/=.
 by case/and3P => /eqP -> /eqP ->.
 Qed.
 
diff --git a/theories/realfun.v b/theories/realfun.v
index 3959a1945..f30276217 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -927,22 +927,22 @@ have [d2 Hd2] : exists d2 : {posnum R},
   rewrite lime_supE => /ereal_inf_lt[x /= [r]]; rewrite in_itv/= andbT.
   by move=> r0 <-{x} H; exists (PosNum r0); rewrite ltW.
 pose d := minr d1%:num d2%:num.
-have d0 : (0 < d)%R by rewrite lt_minr; apply/andP; split => //=.
+have d0 : (0 < d)%R by rewrite lt_min; apply/andP; split => //=.
 move/cvgrPdist_lt : up => /(_ _ d0)[m _] {}ucvg.
 near=> n.
 rewrite /= ler_distlC; apply/andP; split.
   rewrite -lee_fin EFinB (le_trans Hd1)//.
   rewrite (@le_trans _ _ (ereal_inf [set f x | x in ball a d `\ a]))//.
     apply: le_ereal_inf => _/= [r [adr ra] <-]; exists r => //; split => //.
-    by rewrite /ball/= (lt_le_trans adr)// /d le_minl lexx.
+    by rewrite /ball/= (lt_le_trans adr)// /d ge_min lexx.
   apply: ereal_inf_lb => /=; exists (u n).
     split; last by apply/eqP; rewrite eq_sym lt_eqF.
-    by apply: ucvg => //=; near: n; by exists m.
+    by apply: ucvg => //=; near: n; exists m.
   by rewrite fineK//; by near: n.
 rewrite -lee_fin EFinD (le_trans _ Hd2)//.
 rewrite (@le_trans _ _ (ereal_sup [set f x | x in ball a d `\ a]))//; last first.
   apply: le_ereal_sup => z/= [r [adr rp] <-{z}]; exists r => //; split => //.
-  by rewrite /ball/= (lt_le_trans adr)// /d le_minl lexx orbT.
+  by rewrite /ball/= (lt_le_trans adr)// /d ge_min lexx orbT.
 apply: ereal_sup_ub => /=; exists (u n).
   split; last by apply/eqP; rewrite eq_sym lt_eqF.
   by apply: ucvg => //=; near: n; exists m.
@@ -1252,7 +1252,6 @@ have : f a >= f b by rewrite (itvP xfafb).
 by case: ltrgtP xfafb => // ->.
 Qed.
 
-
 Lemma segment_inc_surj_continuous a b f :
     {in `[a, b] &, {mono f : x y / x <= y}} -> set_surj `[a, b] `[f a, f b] f ->
   {within `[a, b], continuous f}.
@@ -1284,10 +1283,10 @@ rewrite ler_distlC; near: y.
 pose u := minr (f x + e%:num / 2) (f b).
 pose l := maxr (f x - e%:num / 2) (f a).
 have ufab : u \in `[f a, f b].
-  rewrite !in_itv /= le_minl ?le_minr lexx ?fle // le_ab orbT ?andbT.
+  rewrite !in_itv /= ge_min ?le_min lexx ?fle // le_ab orbT ?andbT.
   by rewrite ler_wpDr // fle.
 have lfab : l \in `[f a, f b].
-  rewrite !in_itv/= le_maxl ?le_maxr lexx ?fle// le_ab orbT ?andbT.
+  rewrite !in_itv/= ge_max ?le_max lexx ?fle// le_ab orbT ?andbT.
   by rewrite lerBlDr ler_wpDr// fle // lexx.
 have guab : g u \in `[a, b].
   rewrite !in_itv; apply/andP; split; have := ufab; rewrite in_itv => /andP.
@@ -1298,33 +1297,33 @@ have glab : g l \in `[a, b].
     by case; rewrite -[f _ <= _]gle // ?fK // bound_itvE fle.
   by case => _; rewrite -[_ <= f _]gle // ?fK // bound_itvE fle.
 have faltu : f a < u.
-  rewrite /u comparable_lt_minr ?real_comparable ?num_real// flt// aLb andbT.
+  rewrite /u comparable_lt_min ?real_comparable ?num_real// flt// aLb andbT.
   by rewrite (@le_lt_trans _ _ (f x)) ?fle// ltrDl.
 have lltfb : l < f b.
-  rewrite /u comparable_lt_maxl ?real_comparable ?num_real// flt// aLb andbT.
+  rewrite /u comparable_gt_max ?real_comparable ?num_real// flt// aLb andbT.
   by rewrite (@lt_le_trans _ _ (f x)) ?fle// ltrBlDr ltrDl.
 case: pselect => // _; rewrite near_withinE; near_simpl.
 have Fnbhs : Filter (nbhs x) by apply: nbhs_filter.
 have := ax; rewrite le_eqVlt => /orP[/eqP|] {}ax.
   near=> y => /[dup] yab; rewrite /= in_itv => /andP[ay yb]; apply/andP; split.
     by rewrite (@le_trans _ _ (f a)) ?fle// lerBlDr ax ler_wpDr.
-  apply: ltW; suff : f y < u by rewrite lt_minr => /andP[->].
+  apply: ltW; suff : f y < u by rewrite lt_min => /andP[->].
   rewrite -?[f y < _]glt// ?fK//; last by rewrite in_itv /= !fle.
   by near: y; near_simpl; apply: open_lt; rewrite /= -flt ?gK// -ax.
 have := xb; rewrite le_eqVlt => /orP[/eqP {}xb {ax}|{}xb].
   near=> y => /[dup] yab; rewrite /= in_itv /= => /andP[ay yb].
   apply/andP; split; last by rewrite (@le_trans _ _ (f b)) ?fle// xb ler_wpDr.
-  apply: ltW; suff : l < f y by rewrite lt_maxl => /andP[->].
+  apply: ltW; suff : l < f y by rewrite gt_max => /andP[->].
   rewrite -?[_ < f y]glt// ?fK//; last by rewrite in_itv /= !fle.
   by near: y; near_simpl; apply: open_gt; rewrite /= -flt// gK// xb.
 have xoab : x \in `]a, b[ by rewrite in_itv /=; apply/andP; split.
 near=> y; suff: l <= f y <= u.
-  by rewrite le_maxl le_minr -!andbA => /and4P[-> _ ->].
+  by rewrite ge_max le_min -!andbA => /and4P[-> _ ->].
 have ? : y \in `[a, b] by apply: subset_itv_oo_cc; near: y; apply: near_in_itv.
 have fyab : f y \in `[f a, f b] by rewrite in_itv/= !fle// ?ltW.
 rewrite -[l <= _]gle -?[_ <= u]gle// ?fK //.
 apply: subset_itv_oo_cc; near: y; apply: near_in_itv; rewrite in_itv /=.
-rewrite -[x]fK // !glt//= lt_minr lt_maxl ?andbT ltrBlDr ltr_pwDr //.
+rewrite -[x]fK // !glt//= lt_min gt_max ?andbT ltrBlDr ltr_pwDr //.
 by apply/and3P; split; rewrite // flt.
 Unshelve. all: by end_near. Qed.
 
diff --git a/theories/reals.v b/theories/reals.v
index fc47d77dd..8c3d2391c 100644
--- a/theories/reals.v
+++ b/theories/reals.v
@@ -43,6 +43,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra.
 From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval.
+From mathcomp Require Import archimedean.
 
 Require Import Setoid.
 
@@ -119,7 +120,7 @@ End has_bound_lemmas.
 
 (* -------------------------------------------------------------------- *)
 
-HB.mixin Record ArchimedeanField_isReal R of Num.ArchimedeanField R := {
+HB.mixin Record ArchimedeanField_isReal R of Num.ArchiField R := {
   sup_upper_bound_subdef :
     forall E : set [the archiFieldType of R],
       has_sup E -> ubound E (supremum 0 E) ;
@@ -130,7 +131,7 @@ HB.mixin Record ArchimedeanField_isReal R of Num.ArchimedeanField R := {
 
 #[short(type=realType)]
 HB.structure Definition Real := {R of ArchimedeanField_isReal R
-  & Num.ArchimedeanField R & Num.RealClosedField R}.
+  & Num.ArchiField R & Num.RealClosedField R}.
 
 Bind Scope ring_scope with Real.sort.
 
diff --git a/theories/sequences.v b/theories/sequences.v
index 621260f49..b77a383a3 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
-From mathcomp Require Import interval rat.
+From mathcomp Require Import interval rat archimedean.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import set_interval.
 Require Import reals ereal signed topology normedtype landau.
@@ -1264,9 +1264,9 @@ Proof.
 rewrite /series; near \oo => N; have xN : x < N%:R; last first.
   rewrite -(@is_cvg_series_restrict N.+1).
   by apply: (nondecreasing_is_cvgn (incr_S1 N)); eexists; apply: S1_sup.
-near: N; exists (absz (floor x)).+1 => // m; rewrite /mkset -(@ler_nat R).
-move/lt_le_trans => -> //; rewrite (lt_le_trans (lt_succ_floor x)) // -addn1.
-by rewrite natrD lerD2r -(@gez0_abs (floor x)) ?floor_ge0// ltW.
+near: N; exists (absz (reals.floor x)).+1 => // m; rewrite /mkset -(@ler_nat R).
+move/lt_le_trans => -> //; rewrite (lt_le_trans (reals.lt_succ_floor x)) // -addn1.
+by rewrite natrD lerD2r -(@gez0_abs (reals.floor x)) ?reals.floor_ge0// ltW.
 Unshelve. all: by end_near. Qed.
 
 End exponential_series_cvg.
@@ -2113,12 +2113,12 @@ Lemma minr_cvg_0_cvg_0 u r : 0 < r -> (forall k, 0 <= u k) ->
   minr (u n) r @[n --> \oo] --> 0 -> u n @[n --> \oo] --> 0.
 Proof.
 move=> r0 u0 minr_cvg; apply/cvgrPdist_lt => _ /posnumP[e].
-have : 0 < minr e%:num r by rewrite lt_minr// r0 andbT.
+have : 0 < minr e%:num r by rewrite lt_min// r0 andbT.
 move/cvgrPdist_lt : minr_cvg => /[apply] -[M _ hM].
 near=> n; rewrite sub0r normrN.
 have /hM : (M <= n)%N by near: n; exists M.
 rewrite sub0r normrN (ger0_norm (u0 n)) ger0_norm// => [/lt_min_lt//|].
-by rewrite le_minr u0 ltW.
+by rewrite le_min u0 ltW.
 Unshelve. all: by end_near. Qed.
 
 Lemma maxr_cvg_0_cvg_0 u r : r < 0 -> (forall k, u k <= 0) ->
@@ -2148,7 +2148,7 @@ case: x => [r r0 u0 /fine_cvgP[_]|_ u0|//]; last first.
 move=> /cvgrPdist_lt/(_ _ r0)[N _ hN].
 near=> n; have /hN : (N <= n)%N by near: n; exists N.
 rewrite sub0r normrN /= ger0_norm ?fine_ge0//; last first.
-  by rewrite le_minr u0 ltW.
+  by rewrite le_min u0 ltW.
 by have := u0 n; case: (u n) => //=; rewrite ltxx.
 Unshelve. all: by end_near. Qed.
 
diff --git a/theories/signed.v b/theories/signed.v
index 8b3c470f5..de3932d30 100644
--- a/theories/signed.v
+++ b/theories/signed.v
@@ -1096,39 +1096,55 @@ Local Notation nR := {num R & nz & r}.
 Implicit Type x y : nR.
 Local Notation num := (@num _ _ (0 : R) nz r).
 
-Lemma num_le_maxr a x y :
+Lemma num_le_max a x y :
   a <= Num.max x%:num y%:num = (a <= x%:num) || (a <= y%:num).
-Proof. by rewrite -comparable_le_maxr// real_comparable. Qed.
+Proof. by rewrite -comparable_le_max// real_comparable. Qed.
 
-Lemma num_le_maxl a x y :
-  Num.max x%:num  y%:num <= a = (x%:num <= a) && (y%:num <= a).
-Proof. by rewrite -comparable_le_maxl// real_comparable. Qed.
+Lemma num_ge_max a x y :
+  Num.max x%:num y%:num <= a = (x%:num <= a) && (y%:num <= a).
+Proof. by rewrite -comparable_ge_max// real_comparable. Qed.
 
-Lemma num_le_minr a x y :
+Lemma num_le_min a x y :
   a <= Num.min x%:num y%:num = (a <= x%:num) && (a <= y%:num).
-Proof. by rewrite -comparable_le_minr// real_comparable. Qed.
+Proof. by rewrite -comparable_le_min// real_comparable. Qed.
 
-Lemma num_le_minl a x y :
+Lemma num_ge_min a x y :
   Num.min x%:num y%:num <= a = (x%:num <= a) || (y%:num <= a).
-Proof. by rewrite -comparable_le_minl// real_comparable. Qed.
+Proof. by rewrite -comparable_ge_min// real_comparable. Qed.
 
-Lemma num_lt_maxr a x y :
+Lemma num_lt_max a x y :
   a < Num.max x%:num y%:num = (a < x%:num) || (a < y%:num).
-Proof. by rewrite -comparable_lt_maxr// real_comparable. Qed.
+Proof. by rewrite -comparable_lt_max// real_comparable. Qed.
 
-Lemma num_lt_maxl a x y :
+Lemma num_gt_max 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.
+Proof. by rewrite -comparable_gt_max// real_comparable. Qed.
 
-Lemma num_lt_minr a x y :
+Lemma num_lt_min a x y :
   a < Num.min x%:num y%:num = (a < x%:num) && (a < y%:num).
-Proof. by rewrite -comparable_lt_minr// real_comparable. Qed.
+Proof. by rewrite -comparable_lt_min// real_comparable. Qed.
 
-Lemma num_lt_minl a x y :
+Lemma num_gt_min a x y :
   Num.min x%:num y%:num < a = (x%:num < a) || (y%:num < a).
-Proof. by rewrite -comparable_lt_minl// real_comparable. Qed.
+Proof. by rewrite -comparable_gt_min// real_comparable. Qed.
 
 End MorphReal.
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_le_max`")]
+Notation num_le_maxr := num_le_max (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_ge_max`")]
+Notation num_le_maxl := num_ge_max (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_le_min`")]
+Notation num_le_minr := num_le_min (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_ge_min`")]
+Notation num_le_minl := num_ge_min (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lt_max`")]
+Notation num_lt_maxr := num_lt_max (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gt_max`")]
+Notation num_lt_maxl := num_gt_max (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lt_min`")]
+Notation num_lt_minr := num_lt_min (only parsing).
+#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gt_min`")]
+Notation num_lt_minl := num_gt_min (only parsing).
 
 Section MorphGe0.
 Context {R : numDomainType} {nz : nullity}.
diff --git a/theories/topology.v b/theories/topology.v
index 645ef864c..c92ca0ad3 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -1,6 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
+From mathcomp Require Import archimedean.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop.
 Require Import reals signed.
@@ -462,8 +463,8 @@ Proof.
 apply: (iffP idP) => [|[mx|[i Pi mFi]]].
 - rewrite leNgt => /bigmax_ltP /not_andP[/negP|]; first by rewrite -leNgt; left.
   by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -leNgt; right; exists i.
-- by rewrite bigmax_idl le_maxr mx.
-- by rewrite (bigmaxD1 i)// le_maxr mFi.
+- by rewrite bigmax_idl le_max mx.
+- by rewrite (bigmaxD1 i)// le_max mFi.
 Qed.
 
 Lemma bigmax_gtP : reflect (m < x \/ exists2 i, P i & m < F i)
@@ -472,8 +473,8 @@ Proof.
 apply: (iffP idP) => [|[mx|[i Pi mFi]]].
 - rewrite ltNge => /bigmax_leP /not_andP[/negP|]; first by rewrite -ltNge; left.
   by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -ltNge; right; exists i.
-- by rewrite bigmax_idl lt_maxr mx.
-- by rewrite (bigmaxD1 i)// lt_maxr mFi.
+- by rewrite bigmax_idl lt_max mx.
+- by rewrite (bigmaxD1 i)// lt_max mFi.
 Qed.
 
 Lemma bigmin_leP : reflect (x <= m \/ exists2 i, P i & F i <= m)
@@ -482,8 +483,8 @@ Proof.
 apply: (iffP idP) => [|[xm|[i Pi Fim]]].
 - rewrite leNgt => /bigmin_gtP /not_andP[/negP|]; first by rewrite -leNgt; left.
   by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -leNgt; right; exists i.
-- by rewrite bigmin_idl le_minl xm.
-- by rewrite (bigminD1 i)// le_minl Fim.
+- by rewrite bigmin_idl ge_min xm.
+- by rewrite (bigminD1 i)// ge_min Fim.
 Qed.
 
 Lemma bigmin_ltP : reflect (x < m \/ exists2 i, P i & F i < m)
@@ -492,8 +493,8 @@ Proof.
 apply: (iffP idP) => [|[xm|[i Pi Fim]]].
 - rewrite ltNge => /bigmin_geP /not_andP[/negP|]; first by rewrite -ltNge; left.
   by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -ltNge; right; exists i.
-- by rewrite bigmin_idl lt_minl xm.
-- by rewrite (bigminD1 _ _ _ Pi) lt_minl Fim.
+- by rewrite bigmin_idl gt_min xm.
+- by rewrite (bigminD1 _ _ _ Pi) gt_min Fim.
 Qed.
 
 End bigmaxmin.
@@ -4738,7 +4739,7 @@ Proof.
 rewrite entourageE; apply: filter_from_filter; first by exists 1 => /=.
 move=> _ _ /posnumP[e1] /posnumP[e2]; exists (Num.min e1 e2)%:num => //=.
 by rewrite subsetI; split=> ?; apply: ball_le;
-   rewrite num_le// le_minl lexx ?orbT.
+   rewrite num_le// ge_min lexx ?orbT.
 Qed.
 
 Lemma ball_sym_subproof A : ent A -> [set xy | xy.1 = xy.2] `<=` A.
@@ -4989,7 +4990,7 @@ exists (fun n => [set xy : T * T | ball xy.1 n.+1%:R^-1 xy.2]); last first.
 move=> E; rewrite -entourage_ballE => -[e e0 subE].
 exists `|floor e^-1|%N; apply: subset_trans subE => xy; apply: le_ball.
 rewrite /= -[leRHS]invrK lef_pV2 ?posrE ?invr_gt0// -natr1.
-by rewrite natr_absz ger0_norm ?floor_ge0 ?invr_ge0// 1?ltW// lt_succ_floor.
+by rewrite natr_absz ger0_norm ?floor_ge0 ?invr_ge0// 1?ltW// reals.lt_succ_floor.
 Qed.
 
 (** Specific pseudoMetric spaces *)
@@ -5034,18 +5035,24 @@ End matrix_PseudoMetric.
 Section prod_PseudoMetric.
 Context {R : numDomainType} {U V : pseudoMetricType R}.
 Implicit Types (x y : U * V).
+
 Definition prod_point : U * V := (point, point).
+
 Definition prod_ball x (eps : R) y :=
   ball (fst x) eps (fst y) /\ ball (snd x) eps (snd y).
+
 Lemma prod_ball_center x (eps : R) : 0 < eps -> prod_ball x eps x.
 Proof. by move=> /posnumP[?]. Qed.
+
 Lemma prod_ball_sym x y (eps : R) : prod_ball x eps y -> prod_ball y eps x.
 Proof. by move=> [bxy1 bxy2]; split; apply: ball_sym. Qed.
+
 Lemma prod_ball_triangle x y z (e1 e2 : R) :
   prod_ball x e1 y -> prod_ball y e2 z -> prod_ball x (e1 + e2) z.
 Proof.
 by move=> [bxy1 bxy2] [byz1 byz2]; split; apply: ball_triangle; eassumption.
 Qed.
+
 Lemma prod_entourage : entourage = entourage_ prod_ball.
 Proof.
 rewrite predeqE => P; split; last first.
@@ -5059,12 +5066,13 @@ move=> [[_/posnumP[eA] sbA] [_/posnumP[eB] sbB] sABP].
 exists (Num.min eA eB)%:num => //= -[[a b] [c d] [/= bac bbd]].
 suff /sABP [] : (A `*` B) ((a, c), (b, d)) by move=> [[??] [??]] ? [<-<-<-<-].
 split; [apply: sbA|apply: sbB] => /=.
-  by apply: le_ball bac; rewrite num_le le_minl lexx.
-by apply: le_ball bbd; rewrite num_le le_minl lexx orbT.
+  by apply: le_ball bac; rewrite num_le ge_min lexx.
+by apply: le_ball bbd; rewrite num_le ge_min lexx orbT.
 Qed.
 
 HB.instance Definition _ := Uniform_isPseudoMetric.Build R (U * V)%type
   prod_ball_center prod_ball_sym prod_ball_triangle prod_entourage.
+
 End prod_PseudoMetric.
 
 Section Nbhs_fct2.
@@ -5334,10 +5342,10 @@ Global Instance ball_filter (R : realDomainType) (t : R) : Filter
   [set P | exists2 i : R, 0 < i & ball_ Num.norm t i `<=` P].
 Proof.
 apply: Build_Filter; [by exists 1 | move=> P Q | move=> P Q PQ]; rewrite /mkset.
-- move=> -[x x0 xP] [y ? yQ]; exists (Num.min x y); first by rewrite lt_minr x0.
+- move=> -[x x0 xP] [y ? yQ]; exists (Num.min x y); first by rewrite lt_min x0.
   move=> z tz; split.
-    by apply: xP; rewrite /= (lt_le_trans tz) // le_minl lexx.
-  by apply: yQ; rewrite /= (lt_le_trans tz) // le_minl lexx orbT.
+    by apply: xP; rewrite /= (lt_le_trans tz) // ge_min lexx.
+  by apply: yQ; rewrite /= (lt_le_trans tz) // ge_min lexx orbT.
 - by move=> -[x ? xP]; exists x => //; apply: (subset_trans xP).
 Qed.
 
@@ -5670,7 +5678,7 @@ Local Open Scope ring_scope.
 Local Definition distN (e : R) : nat := `|floor e^-1|%N.
 
 Local Lemma distN0 : distN 0 = 0%N.
-Proof. by rewrite /distN invr0 floor0. Qed.
+Proof. by rewrite /distN invr0 reals.floor0. Qed.
 
 Local Lemma distN_nat (n : nat): distN (n%:R^-1) = n.
 Proof.
diff --git a/theories/trigo.v b/theories/trigo.v
index b82dad0d8..00e542f9c 100644
--- a/theories/trigo.v
+++ b/theories/trigo.v
@@ -568,7 +568,7 @@ Qed.
 Lemma cos_exists : exists2 pih : R, 1 <= pih <= 2 & cos pih = 0.
 Proof.
 have /IVT[] : minr (cos 1) (cos 2) <= (0 : R) <= maxr (cos 1) (cos 2).
-  - by rewrite le_maxr (ltW cos1_gt0) le_minl (ltW cos2_lt0) orbC.
+  - by rewrite le_max (ltW cos1_gt0) ge_min (ltW cos2_lt0) orbC.
   - by rewrite ler1n.
   - by apply/continuous_subspaceT => ?; exact: continuous_cos.
 by move=> pih /itvP pihI chpi_eq0; exists pih; rewrite ?pihI.