diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index b05b5aece..6ebeba83c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -132,6 +132,12 @@
   + `lte_le_sub` -> `lte_leB`
   + `lte_le_dsub` -> `lte_le_dB`
 
+- in `reals.v`:
+  + `inf_lb` -> `inf_lbound`
+  + `sup_ub` -> `sup_ubound`
+  + `ereal_inf_lb` -> `ereal_inf_lbound`
+  + `ereal_sup_ub` -> `ereal_sup_ubound`
+
 ### Generalized
 
 - in `constructive_ereal.v`:
diff --git a/theories/charge.v b/theories/charge.v
index 090a26246..9a9c35efd 100644
--- a/theories/charge.v
+++ b/theories/charge.v
@@ -630,7 +630,7 @@ Let subDD A := [set nu E | E in [set E | measurable E /\ E `<=` D `\` A] ].
 Let d_ A := ereal_sup (subDD A).
 
 Let d_ge0 X : 0 <= d_ X.
-Proof. by apply: ereal_sup_ub => /=; exists set0; rewrite ?charge0. Qed.
+Proof. by apply: ereal_sup_ubound => /=; exists set0; rewrite ?charge0. Qed.
 
 Let elt_rel i j :=
   [/\ g_ j = d_ (U_ i),  A_ j `<=` D `\` U_ i & U_ j = U_ i `|` A_ j ].
@@ -714,7 +714,7 @@ have EH n : [set nu E] `<=` H n.
   by apply: (subset_trans FDAoo); apply: setDS; exact: bigsetU_bigcup.
 have nudelta n : nu E <= g_ (v n).
   move: n => [|n].
-    rewrite v0/=; apply: ereal_sup_ub => /=; exists E; split => //.
+    rewrite v0/=; apply: ereal_sup_ubound => /=; exists E; split => //.
     by apply: (subset_trans EDAoo); exact: setDS.
   suff : nu E <= d_ (U_ (v n)) by have [<- _] := Pv n.
   have /le_ereal_sup := EH n.+1; rewrite ereal_sup1 => /le_trans; apply.
@@ -763,7 +763,7 @@ Let s_ A := ereal_inf (subC A).
 
 Let s_le0 X : s_ X <= 0.
 Proof.
-by apply: ereal_inf_lb => /=; exists set0; rewrite ?charge0//=; split.
+by apply: ereal_inf_lbound => /=; exists set0; rewrite ?charge0//=; split.
 Qed.
 
 Let elt_rel i j :=
@@ -813,8 +813,9 @@ exists P, N; split; [|exact: neg_set_N|by rewrite /P setvU|by rewrite /P setICl]
 split=> // D mD DP; rewrite leNgt; apply/negP => nuD0.
 have znuD n : z_ (v n) <= nu D.
   move: n => [|n].
-    by rewrite v0 /=; apply: ereal_inf_lb; exists D; split => //; rewrite setC0.
-  have [-> _ _] := Pv n; apply: ereal_inf_lb => /=; exists D; split => //.
+    rewrite v0 /=; apply: ereal_inf_lbound; exists D; split => //.
+    by rewrite setC0.
+  have [-> _ _] := Pv n; apply: ereal_inf_lbound => /=; exists D; split => //.
   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.
@@ -1277,7 +1278,7 @@ Let M_g_F m : M - m.+1%:R^-1%:E < \int[mu]_x g m x /\
 Proof.
 split; first by have [] := approxRN_seq_prop mu nu m.
 apply/andP; split; last first.
-  by apply: ereal_sup_ub; exists (F m)  => //; have := F_G m; rewrite inE.
+  by apply: ereal_sup_ubound; exists (F m)  => //; have := F_G m; rewrite inE.
 apply: ge0_le_integral => //.
 - by move=> x _; exact: approxRN_seq_ge0.
 - exact: measurable_approxRN_seq.
diff --git a/theories/ereal.v b/theories/ereal.v
index 414423e22..0ae89ce34 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -503,7 +503,7 @@ move/sup_upper_bound/ubP; apply.
 by case: y' Sy' => [r1 /= Sr1 | // | /= _]; [exists r1%:E | exists r%:E].
 Qed.
 
-Lemma ereal_sup_ub S : ubound S (ereal_sup S).
+Lemma ereal_sup_ubound S : ubound S (ereal_sup S).
 Proof.
 move=> y Sy; rewrite /ereal_sup /supremum ifF; last first.
   by apply/eqP; rewrite predeqE => /(_ y)[+ _]; exact.
@@ -513,35 +513,39 @@ Qed.
 
 Lemma ereal_supy S : S +oo -> ereal_sup S = +oo.
 Proof.
-by move=> Soo; apply/eqP; rewrite eq_le leey/=; exact: ereal_sup_ub.
+by move=> Soo; apply/eqP; rewrite eq_le leey/=; exact: ereal_sup_ubound.
 Qed.
 
 Lemma ereal_sup_le S x : (exists2 y, S y & x <= y) -> x <= ereal_sup S.
-Proof. by move=> [y Sy] /le_trans; apply; exact: ereal_sup_ub. Qed.
+Proof. by move=> [y Sy] /le_trans; apply; exact: ereal_sup_ubound. Qed.
 
 Lemma ereal_sup_ninfty S : ereal_sup S = -oo <-> S `<=` [set -oo].
 Proof.
 split.
-  by move=> supS [r /ereal_sup_ub | /ereal_sup_ub |//]; rewrite supS.
-move=> /(@subset_set1 _ S) [] ->; [exact: ereal_sup0|exact: ereal_sup1].
+  by move=> supS [r /ereal_sup_ubound|/ereal_sup_ubound|//]; rewrite supS.
+by move=> /(@subset_set1 _ S) [] ->; [exact: ereal_sup0|exact: ereal_sup1].
 Qed.
 
-Lemma ereal_inf_lb S : lbound S (ereal_inf S).
+Lemma ereal_inf_lbound S : lbound S (ereal_inf S).
 Proof.
-by move=> x Sx; rewrite /ereal_inf leeNl; apply ereal_sup_ub; exists x.
+by move=> x Sx; rewrite /ereal_inf leeNl; apply: ereal_sup_ubound; exists x.
 Qed.
 
 Lemma ereal_inf_le S x : (exists2 y, S y & y <= x) -> ereal_inf S <= x.
-Proof. by move=> [y Sy]; apply: le_trans; exact: ereal_inf_lb. Qed.
+Proof. by move=> [y Sy]; apply: le_trans; exact: ereal_inf_lbound. Qed.
 
 Lemma ereal_inf_pinfty S : ereal_inf S = +oo <-> S `<=` [set +oo].
 Proof. rewrite eqe_oppLRP oppe_subset image_set1; exact: ereal_sup_ninfty. Qed.
 
 Lemma le_ereal_sup : {homo @ereal_sup R : A B / A `<=` B >-> A <= B}.
-Proof. by move=> A B AB; apply: ub_ereal_sup => x Ax; apply/ereal_sup_ub/AB. Qed.
+Proof.
+by move=> A B AB; apply: ub_ereal_sup => x Ax; exact/ereal_sup_ubound/AB.
+Qed.
 
 Lemma le_ereal_inf : {homo @ereal_inf R : A B / A `<=` B >-> B <= A}.
-Proof. by move=> A B AB; apply: lb_ereal_inf => x Bx; exact/ereal_inf_lb/AB. Qed.
+Proof.
+by move=> A B AB; apply: lb_ereal_inf => x Bx; exact/ereal_inf_lbound/AB.
+Qed.
 
 Lemma hasNub_ereal_sup (A : set R) : ~ has_ubound A ->
   A !=set0 -> ereal_sup (EFin @` A) = +oo%E.
@@ -549,7 +553,7 @@ Proof.
 move=> + A0; apply: contra_notP => /eqP; rewrite -ltey => Aoo.
 exists (fine (ereal_sup (EFin @` A))) => x Ax.
 rewrite -lee_fin -(@fineK _ x%:E)// lee_fin fine_le//; last first.
-  by apply: ereal_sup_ub => /=; exists x.
+  by apply: ereal_sup_ubound => /=; exists x.
 rewrite fin_numE// -ltey Aoo andbT.
 apply/eqP => /ereal_sup_ninfty/(_ x%:E).
 by have /[swap] /[apply]: (EFin @` A) x%:E by exists x.
@@ -559,7 +563,7 @@ Lemma ereal_sup_EFin (A : set R) :
   has_ubound A -> A !=set0 -> ereal_sup (EFin @` A) = (sup A)%:E.
 Proof.
 move=> has_ubA A0; apply/eqP; rewrite eq_le; apply/andP; split.
-  by apply: ub_ereal_sup => /= y [r Ar <-{y}]; rewrite lee_fin sup_ub.
+  by apply: ub_ereal_sup => /= y [r Ar <-{y}]; rewrite lee_fin sup_ubound.
 set esup := ereal_sup _; have := leey esup.
 rewrite le_eqVlt => /predU1P[->|esupoo]; first by rewrite leey.
 have := leNye esup; rewrite le_eqVlt => /predU1P[/esym|ooesup].
@@ -569,7 +573,7 @@ have esup_fin_num : esup \is a fin_num.
   by rewrite fin_numE -leeNy_eq -ltNge ooesup /= -leye_eq -ltNge esupoo.
 rewrite -(@fineK _ esup) // lee_fin leNgt.
 apply/negP => /(sup_gt A0)[r Ar]; apply/negP; rewrite -leNgt.
-by rewrite -lee_fin fineK//; apply: ereal_sup_ub; exists r.
+by rewrite -lee_fin fineK//; apply: ereal_sup_ubound; exists r.
 Qed.
 
 Lemma ereal_inf_EFin (A : set R) : has_lbound A -> A !=set0 ->
@@ -581,6 +585,10 @@ by rewrite !image_comp.
 Qed.
 
 End ereal_supremum_realType.
+#[deprecated(since="mathcomp-analysis 1.3.0", note="Renamed `ereal_sup_ubound`.")]
+Notation ereal_sup_ub := ereal_sup_ubound (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="Renamed `ereal_inf_lbound`.")]
+Notation ereal_inf_lb := ereal_inf_lbound (only parsing).
 
 Lemma restrict_abse T (R : numDomainType) (f : T -> \bar R) (D : set T) :
   (abse \o f) \_ D = abse \o (f \_ D).
@@ -931,16 +939,16 @@ case=> x Sx; rewrite ler_norml; apply/andP; split; last first.
   by move=> r [y Sy] <-; case/ler_normlP : (contract_le1 y).
 rewrite (@le_trans _ _ (contract x)) //.
   by case/ler_normlP : (contract_le1 x); rewrite lerNl.
-apply sup_ub; last by exists x.
+apply: sup_ubound; last by exists x.
 by exists 1%R => r [y Sy <-]; case/ler_normlP : (contract_le1 y).
 Qed.
 
 Lemma contract_sup S : S !=set0 -> contract (ereal_sup S) = sup (contract @` S).
 Proof.
 move=> S0; apply/eqP; rewrite eq_le; apply/andP; split; last first.
-  apply sup_le_ub.
+  apply: sup_le_ub.
     by case: S0 => x Sx; exists (contract x), x.
-  move=> x [y Sy] <-{x}; rewrite le_contract; exact/ereal_sup_ub.
+  by move=> x [y Sy] <-{x}; rewrite le_contract; exact/ereal_sup_ubound.
 rewrite leNgt; apply/negP.
 set supc := sup _; set csup := contract _; move=> ltsup.
 suff [y [ysupS ?]] : exists y, y < ereal_sup S /\ ubound S y.
@@ -954,7 +962,7 @@ suff [x [? [ubSx x1]]] : exists x, (x < csup)%R /\ ubound (contract @` S) x /\
 exists ((supc + csup) / 2); split; first by rewrite midf_lt.
 split => [r [y Sy <-{r}]|].
   rewrite (@le_trans _ _ supc) ?midf_le //; last by rewrite ltW.
-  apply sup_ub; last by exists y.
+  apply: sup_ubound; last by exists y.
   by exists 1%R => r [z Sz <-]; case/ler_normlP : (contract_le1 z).
 rewrite ler_norml; apply/andP; split; last first.
   rewrite ler_pdivrMr // mul1r (_ : 2 = 1 + 1)%R // lerD //.
@@ -968,7 +976,8 @@ Qed.
 Lemma contract_inf S : S !=set0 -> contract (ereal_inf S) = inf (contract @` S).
 Proof.
 move=> -[x Sx]; rewrite /ereal_inf /contract (contractN (ereal_sup (-%E @` S))).
-by rewrite -/contract contract_sup /inf; [rewrite contract_imageN | exists (- x), x].
+by rewrite -/contract contract_sup /inf;
+  [rewrite contract_imageN|exists (- x), x].
 Qed.
 
 End contract_expand_realType.
@@ -1020,7 +1029,7 @@ Lemma ball_ereal_ball_fin_lt r r' (e : {posnum R}) :
   let e' := (r - fine (expand (contract r%:E - e%:num)))%R in
   ball r e' r' -> (r' < r)%R ->
   (`|contract r%:E - (e)%:num| < 1)%R ->
-  ereal_ball r%:E (e)%:num r'%:E.
+  ereal_ball r%:E e%:num r'%:E.
 Proof.
 move=> e' re'r' rr' X; rewrite /ereal_ball.
 rewrite gtr0_norm ?subr_gt0// ?lt_contract ?lte_fin//.
@@ -1035,7 +1044,7 @@ Lemma ball_ereal_ball_fin_le r r' (e : {posnum R}) :
   let e' : R := (fine (expand (contract r%:E + e%:num)) - r)%R in
   ball r e' r' -> (r <= r')%R ->
   (`| contract r%:E + e%:num | < 1)%R ->
-  (ereal_ball r%:E e%:num r'%:E).
+  ereal_ball r%:E e%:num r'%:E.
 Proof.
 move=> e' r'e'r rr' re1; rewrite /ereal_ball.
 move: rr'; rewrite le_eqVlt => /predU1P[->|rr']; first by rewrite subrr normr0.
@@ -1321,8 +1330,7 @@ rewrite predeq2E => x A; split.
       apply: MA; rewrite lte_fin.
       rewrite ger0_norm in rM1; last first.
         by rewrite subr_ge0 // (le_trans _ (contract_le1 r%:E)) // ler_norm.
-      rewrite ltrBlDr addrC addrCA addrC -ltrBlDr subrr in rM1.
-      rewrite subr_gt0 in rM1.
+      rewrite ltrBlDr addrC addrCA addrC -ltrBlDr subrr subr_gt0 in rM1.
       by rewrite -lte_fin -lt_contract.
     * by rewrite /ereal_ball /= subrr normr0 => h; exact: MA.
     * rewrite /ereal_ball /= opprK => h {MA}.
diff --git a/theories/esum.v b/theories/esum.v
index 95e7d038e..9df507fb1 100644
--- a/theories/esum.v
+++ b/theories/esum.v
@@ -79,7 +79,7 @@ Implicit Types (a : T -> \bar R).
 Lemma esum_ge0 (S : set T) a :
   (forall x, S x -> 0 <= a x) -> 0 <= \esum_(i in S) a i.
 Proof.
-move=> a0; apply: ereal_sup_ub.
+move=> a0; apply: ereal_sup_ubound.
 by exists set0; [exact: fsets_set0|rewrite fsbig_set0].
 Qed.
 
@@ -88,7 +88,7 @@ Lemma esum_fset (F : set T) a : finite_set F ->
   \esum_(i in F) a i = \sum_(i \in F) a i.
 Proof.
 move=> finF f0; apply/eqP; rewrite eq_le; apply/andP; split; last first.
-  by apply ereal_sup_ub; exists F => //; exact: fsets_self.
+  by apply: ereal_sup_ubound; exists F => //; exact: fsets_self.
 apply ub_ereal_sup => /= ? -[F' [finF' F'F] <-].
 apply/lee_fsum_nneg_subset => //; first exact/subsetP.
 by  move=> t; rewrite inE/= => /andP[_] /f0.
@@ -101,11 +101,6 @@ Qed.
 
 End esum_realType.
 
-Lemma esum_ge [R : realType] [T : choiceType] (I : set T) (a : T -> \bar R) x :
-  (exists2 X : set T, fsets I X & x <= \sum_(i \in X) a i) ->
-  x <= \esum_(i in I) a i.
-Proof. by move=> [X IX /le_trans->//]; apply: ereal_sup_ub => /=; exists X. Qed.
-
 Lemma esum1 [R : realFieldType] [I : choiceType] (D : set I) (a : I -> \bar R) :
   (forall i, D i -> a i = 0) -> \esum_(i in D) a i = 0.
 Proof.
@@ -115,6 +110,11 @@ apply/seteqP; split=> x //= => [[X [finX XI]] <-|->].
 by exists set0; rewrite ?fsbig_set0//; exact: fsets_set0.
 Qed.
 
+Lemma esum_ge [R : realType] [T : choiceType] (I : set T) (a : T -> \bar R) x :
+  (exists2 X : set T, fsets I X & x <= \sum_(i \in X) a i) ->
+  x <= \esum_(i in I) a i.
+Proof. by move=> [X IX /le_trans->//]; apply: ereal_sup_ubound; exists X. Qed.
+
 Lemma le_esum [R : realType] [T : choiceType] (I : set T) (a b : T -> \bar R) :
   (forall i, I i -> a i <= b i) ->
   \esum_(i in I) a i <= \esum_(i in I) b i.
@@ -134,7 +134,7 @@ Lemma esumD [R : realType] [T : choiceType] (I : set T) (a b : T -> \bar R) :
 Proof.
 move=> ag0 bg0; apply/eqP; rewrite eq_le; apply/andP; split.
   rewrite ub_ereal_sup//= => x [X [finX XI]] <-; rewrite fsbig_split//=.
-  by rewrite leeD// ereal_sup_ub//=; exists X.
+  by rewrite leeD// ereal_sup_ubound//=; exists X.
 wlog : a b ag0 bg0 / \esum_(i in I) a i \isn't a fin_num => [saoo|]; last first.
   move=> /fin_numPn[->|/[dup] aoo ->]; first by rewrite leNye.
   rewrite (@le_trans _ _ +oo)//; first by rewrite /adde/=; case: esum.
@@ -156,11 +156,12 @@ have saX : \sum_(i \in X) a i \is a fin_num.
 rewrite leeBrDr// addeC -leeBrDr// ub_ereal_sup//= => _ [Y [finY YI]] <-.
 rewrite leeBrDr// addeC esum_ge//; exists (X `|` Y).
   by split; [rewrite finite_setU|rewrite subUset].
-rewrite fsbig_split ?finite_setU//= leeD// lee_fsum_nneg_subset//= ?finite_setU//.
+rewrite fsbig_split ?finite_setU//= leeD// lee_fsum_nneg_subset ?finite_setU//=.
 - exact/subsetP/subsetUl.
-- by move=> x; rewrite !inE in_setU andb_orr andNb/= => /andP[_] /[!inE] /YI/ag0.
+- by move=> x; rewrite !inE in_setU andb_orr andNb => /andP[_] /[!inE] /YI/ag0.
 - exact/subsetP/subsetUr.
-- by move=> x; rewrite !inE in_setU andb_orr andNb/= orbF => /andP[_] /[!inE] /XI/bg0.
+- move=> x; rewrite !inE in_setU andb_orr andNb/= orbF.
+  by move=> /andP[_] /[!inE] /XI/bg0.
 Qed.
 
 Lemma esum_mkcond [R : realType] [T : choiceType] (I : set T)
@@ -169,20 +170,23 @@ Lemma esum_mkcond [R : realType] [T : choiceType] (I : set T)
 Proof.
 apply/eqP; rewrite eq_le !ub_ereal_sup//= => _ [X [finX XI]] <-.
   rewrite -big_mkcond/= big_fset_condE/=; set Y := [fset _ | _ in _ & _]%fset.
-  rewrite ereal_sup_ub//=; exists [set` Y]; last by rewrite fsbig_finite// set_fsetK.
-  by split => // i/=; rewrite !inE/= => /andP[_]; rewrite inE.
-rewrite ereal_sup_ub//; exists X => //; apply: eq_fsbigr => x; rewrite inE => Xx.
+  rewrite ereal_sup_ubound//=; exists [set` Y].
+    by split => // i/=; rewrite !inE/= => /andP[_]; rewrite inE.
+  by rewrite fsbig_finite// set_fsetK.
+rewrite ereal_sup_ubound//; exists X => //; apply: eq_fsbigr => x /[!inE] Xx.
 by rewrite ifT// inE; exact: XI.
 Qed.
 
-Lemma esum_mkcondr [R : realType] [T : choiceType] (I J : set T) (a : T -> \bar R) :
+Lemma esum_mkcondr [R : realType] [T : choiceType] (I J : set T)
+    (a : T -> \bar R) :
   \esum_(i in I `&` J) a i = \esum_(i in I) if i \in J then a i else 0.
 Proof.
 rewrite esum_mkcond [RHS]esum_mkcond; apply: eq_esum=> i _.
 by rewrite in_setI; case: (i \in I) (i \in J) => [] [].
 Qed.
 
-Lemma esum_mkcondl [R : realType] [T : choiceType] (I J : set T) (a : T -> \bar R) :
+Lemma esum_mkcondl [R : realType] [T : choiceType] (I J : set T)
+    (a : T -> \bar R) :
   \esum_(i in I `&` J) a i = \esum_(i in J) if i \in I then a i else 0.
 Proof.
 rewrite esum_mkcond [RHS]esum_mkcond; apply: eq_esum=> i _.
@@ -208,7 +212,7 @@ Lemma esum_sum [R : realType] [T1 T2 : choiceType]
 Proof.
 move=> a_ge0; elim: r => [|j r IHr]; rewrite ?(big_nil, big_cons)// -?IHr.
   by rewrite esum1// => i; rewrite big_nil.
-case: (boolP (P j)) => Pj; last first.
+case: ifPn => Pj; last first.
   by apply: eq_esum => i Ii; rewrite big_cons (negPf Pj).
 have aj_ge0 i : I i -> a i j >= 0 by move=> ?; apply: a_ge0.
 rewrite -esumD//; last by move=> i Ii; apply: sume_ge0 => *; apply: a_ge0.
@@ -227,7 +231,7 @@ move=> a_ge0; apply/eqP; rewrite eq_le; apply/andP; split.
     move=> i j _ /[!in_fset_set]// /[!inE] /XI Ij.
     by case: ifPn => // /[!inE] /a_ge0-/(_ Ij).
   under eq_esum do rewrite -big_seq -big_mkcond/=.
-  apply: ub_ereal_sup => /= _ [Y [finY _] <-]; apply: ereal_sup_ub => /=.
+  apply: ub_ereal_sup => /= _ [Y [finY _] <-]; apply: ereal_sup_ubound => /=.
   set XYJ := [set z | z \in X `*` Y /\ z.2 \in J z.1].
   have ? : finite_set XYJ.
     apply: sub_finite_set (finite_setM finX finY) => z/=.
@@ -266,7 +270,7 @@ apply: (@le_trans _ _
   by rewrite mem_set//; move/XIJ : Xij => [].
 rewrite -fsbig_finite; last exact: finite_set_fst.
 apply lee_fsum=> [|i Xi]; first exact: finite_set_fst.
-rewrite ereal_sup_ub => //=; have ? : finite_set (X.`2 `&` J i).
+rewrite ereal_sup_ubound //=; have ? : finite_set (X.`2 `&` J i).
   by apply: finite_setI; left; exact: finite_set_snd.
 exists (X.`2 `&` J i) => //.
 rewrite [in RHS]big_fset_condE/= fsbig_finite//; apply eq_fbigl => j.
@@ -308,10 +312,11 @@ Lemma nneseries_esum (R : realType) (a : nat -> \bar R) (P : pred nat) :
 Proof.
 move=> a0; apply/eqP; rewrite eq_le; apply/andP; split.
   apply: (lime_le (is_cvg_nneseries_cond a0)); apply: nearW => n.
-  apply: ereal_sup_ub => /=; exists [set` [fset val i | i in 'I_n & P i]%fset].
+  apply: ereal_sup_ubound; exists [set` [fset val i | i in 'I_n & P i]%fset].
     split; first exact: finite_fset.
     by move=> /= k /imfsetP[/= i]; rewrite inE => + ->.
-  rewrite fsbig_finite//= set_fsetK big_imfset/=; last by move=> ? ? ? ? /val_inj.
+  rewrite fsbig_finite//= set_fsetK big_imfset/=; last first.
+    by move=> ? ? ? ? /val_inj.
   by rewrite big_filter big_enum_cond/= big_mkord.
 apply: ub_ereal_sup => _ [/= F [finF PF] <-].
 rewrite fsbig_finite//= -(big_rmcond_in P)/=; first exact: lee_sum_fset_lim.
@@ -334,7 +339,7 @@ gen have le_esum : T T' a P Q e /
   rewrite [leRHS](_ : _ = \esum_(j in Q) a (e (e^-1%FUN j))); last first.
     by apply: eq_esum => i Qi; rewrite invK ?inE.
   by rewrite le_esum => //= i Qi; rewrite a_ge0//; exact: funS.
-rewrite ub_ereal_sup => //= _ [X [finX XQ] <-]; rewrite ereal_sup_ub => //=.
+rewrite ub_ereal_sup => //= _ [X [finX XQ] <-]; rewrite ereal_sup_ubound => //=.
 exists [set` (e^-1 @` (fset_set X))%fset].
   split=> [|t /= /imfsetP[t'/=]]; first exact: finite_fset.
   by rewrite in_fset_set// inE => /XQ Qt' ->; exact: funS.
diff --git a/theories/kernel.v b/theories/kernel.v
index d930e6ca9..1dcd54c6e 100644
--- a/theories/kernel.v
+++ b/theories/kernel.v
@@ -368,7 +368,7 @@ HB.builders Context d d' (X : measurableType d) (Y : measurableType d')
 Let finite : @Kernel_isFinite d d' X Y R k.
 Proof.
 split; exists 2%R => /= ?; rewrite (@le_lt_trans _ _ 1%:E) ?lte_fin ?ltr1n//.
-by rewrite (le_trans _ sprob_kernel)//; exact: ereal_sup_ub.
+by rewrite (le_trans _ sprob_kernel)//; exact: ereal_sup_ubound.
 Qed.
 
 HB.instance Definition _ := finite.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 58fdb451b..7bf196bac 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -939,7 +939,7 @@ Variable (mu : {measure set T -> \bar R}).
 
 Let nnintegral_ge0 f : (forall x, 0 <= f x) -> 0 <= nnintegral mu f.
 Proof.
-by move=> f0; apply: ereal_sup_ub; exists nnsfun0; last by rewrite sintegral0.
+by move=> f0; apply: ereal_sup_ubound; exists nnsfun0 => //; exact: sintegral0.
 Qed.
 
 Let eq_nnintegral g f : f =1 g -> nnintegral mu f = nnintegral mu g.
@@ -948,8 +948,7 @@ Proof. by move=> /funext->. Qed.
 Let nnintegral0 : nnintegral mu (cst 0) = 0.
 Proof.
 rewrite /nnintegral /=; apply/eqP; rewrite eq_le; apply/andP; split; last first.
-  apply/ereal_sup_ub; exists nnsfun0; last by rewrite sintegral0.
-  by [].
+  by apply/ereal_sup_ubound; exists nnsfun0; [|exact: sintegral0].
 apply/ub_ereal_sup => /= x [f /= f0 <-]; have {}f0 : forall x, f x = 0%R.
   by move=> y; apply/eqP; rewrite eq_le -2!lee_fin f0 //= lee_fin//.
 by rewrite (eq_sintegral (@nnsfun0 _ T R)) ?sintegral0.
@@ -960,7 +959,7 @@ Let nnintegral_nnsfun (h : {nnsfun T >-> R}) :
 Proof.
 apply/eqP; rewrite eq_le; apply/andP; split.
   by apply/ub_ereal_sup => /= _ -[g /= gh <-]; rewrite le_sintegral.
-by apply: ereal_sup_ub => /=; exists h.
+by apply: ereal_sup_ubound => /=; exists h.
 Qed.
 
 Local Notation "\int_ ( x 'in' D ) F" := (integral mu D (fun x => F))
@@ -1125,11 +1124,11 @@ Proof.
 rewrite ge0_integralTE//.
 apply/eqP; rewrite eq_le; apply/andP; split; last first.
   apply: lime_le; first exact: is_cvg_sintegral.
-  near=> n; apply: ereal_sup_ub; exists (g n) => //= => x.
+  near=> n; apply: ereal_sup_ubound; exists (g n) => //= => x.
   have <- : limn (EFin \o g ^~ x) = f x by apply/cvg_lim => //; exact: gf.
   have : EFin \o g ^~ x @ \oo --> ereal_sup (range (EFin \o g ^~ x)).
     by apply: ereal_nondecreasing_cvgn => p q pq /=; rewrite lee_fin; exact/nd_g.
-  by move/cvg_lim => -> //; apply: ereal_sup_ub; exists n.
+  by move/cvg_lim => -> //; apply: ereal_sup_ubound; exists n.
 have := leey (\int[mu]_x (f x)).
 rewrite le_eqVlt => /predU1P[|] mufoo; last first.
   have : \int[mu]_x (f x) \is a fin_num by rewrite ge0_fin_numE// integral_ge0.
@@ -1632,7 +1631,7 @@ have [g1 [nd_g1 /(_ _ Logic.I)gh1]] :=
 rewrite (nd_ge0_integral_lim _ h10 (fun x => lef_at x nd_g1) gh1)//.
 apply: lime_le.
   by apply: is_cvg_sintegral => // t Dt; exact/(lef_at t nd_g1).
-near=> n; rewrite ge0_integralTE//; apply: ereal_sup_ub => /=.
+near=> n; rewrite ge0_integralTE//; apply: ereal_sup_ubound => /=.
 exists (g1 n) => // t; rewrite (le_trans _ (h12 _)) //.
 have := gh1 t.
 have := leey (h1 t); rewrite le_eqVlt => /predU1P[->|ftoo].
@@ -1752,7 +1751,7 @@ move=> D [/= mD Deps KDf]; exists (K `\` D); split => //.
 - exact: subset_trans Kab.
 - rewrite setDDr; apply: le_lt_trans => /=.
     by apply: measureU2 => //; apply: measurableI => //; apply: measurableC.
-  rewrite [_%:num]splitr EFinD; apply: lee_lt_add => //=; first 2 last.
+  rewrite [_%:num]splitr EFinD; apply: lee_ltD => //=; first 2 last.
   + by rewrite (@le_lt_trans _ _ (mu D)) ?le_measure ?inE//; exact: measurableI.
   + rewrite ge0_fin_numE// (@le_lt_trans _ _ (mu A))// le_measure ?inE//.
     exact: measurableD.
@@ -2173,7 +2172,7 @@ apply: lee_lim.
 - apply: ereal_nondecreasing_is_cvgn => // n m nm; apply: ge0_le_integral => //.
   by move=> *; exact/nd_g.
 - apply: nearW => n; rewrite ge0_integralTE//.
-  by apply: ereal_sup_ub; exists (max_g2 n) => // t; exact: max_g2_g.
+  by apply: ereal_sup_ubound; exists (max_g2 n) => // t; exact: max_g2_g.
 Unshelve. all: by end_near. Qed.
 
 Lemma cvg_monotone_convergence :
@@ -2428,7 +2427,7 @@ apply: lee_lim.
       \int[mu]_(x in D) g n x <= einfs (fun k => \int[mu]_(x in D) f k x) n.
     move=> n p np; apply: lb_ereal_inf => /= _ [k /= nk <-].
     apply: ge0_le_integral => //; [exact: g0|exact: mg|exact: f0|].
-    by move=> x Dx; apply: ereal_inf_lb; exists k.
+    by move=> x Dx; apply: ereal_inf_lbound; exists k.
   exact.
 Qed.
 
@@ -2688,7 +2687,7 @@ move=> f0 mf.
 have [f_ [f_nd f_f]] := approximation mD mf f0.
 elim => [|N ih]; first by rewrite big_ord0 msum_mzero integral_measure_zero.
 rewrite big_ord_recr/= -ih.
-rewrite (_ : _ m_ N.+1 = measure_add [the measure _ _ of msum m_ N] (m_ N)); last first.
+rewrite (_ : _ m_ N.+1 = measure_add (msum m_ N) (m_ N)); last first.
   by apply/funext => A; rewrite measure_addE /msum/= big_ord_recr.
 have mf_ n : measurable_fun D (fun x => (f_ n x)%:E).
   exact/measurable_funTS/EFin_measurable_fun.
@@ -3210,9 +3209,9 @@ have lim_f_ t : f_ ^~ t @ \oo --> (f \_ D) t.
   rewrite [X in _ --> X](_ : _ = ereal_sup (range (f_ ^~ t))); last first.
     apply/eqP; rewrite eq_le; apply/andP; split.
       rewrite /restrict; case: ifPn => [|_].
-        rewrite in_setE => -[n _ Fnt]; apply: ereal_sup_ub; exists n.+1 => //.
+        rewrite in_setE => -[n _ Fnt]; apply: ereal_sup_ubound; exists n.+1=>//.
         by rewrite /f_ big_mkord patchT// in_setE big_ord_recr/=; right.
-      rewrite (@le_trans _ _ (f_ O t))// ?ereal_sup_ub//.
+      rewrite (@le_trans _ _ (f_ O t))// ?ereal_sup_ubound//.
       by rewrite /f_ patchN// big_mkord big_ord0 inE/= in_set0.
     apply: ub_ereal_sup => x [n _ <-].
     by rewrite /f_ restrict_lee// big_mkord; exact: bigsetU_bigcup.
@@ -5910,7 +5909,7 @@ move: a0; rewrite le_eqVlt => /predU1P[a0|a0].
     apply: measurable_funTS; apply: measurableT_comp => //=.
     by apply/measurableT_comp => //=; case: locf.
   have : iavg f (ball y (r + d)) <= HL f y.
-    apply: ereal_sup_ub => /=; exists (r + d)%R => //.
+    apply: ereal_sup_ubound => /=; exists (r + d)%R => //.
     by rewrite in_itv/= andbT addr_gt0.
   apply/lt_le_trans/(lt_le_trans xrdk); rewrite /iavg.
   do 2 (rewrite lebesgue_measure_ball; last by rewrite addr_ge0// ltW).
@@ -5954,7 +5953,7 @@ have /lt_le_trans : a%:E < iavg f (ball y (r + d)).
   do 2 (rewrite lebesgue_measure_ball; last by rewrite addr_ge0// ltW).
   rewrite lee_wpmul2l// lee_fin invr_ge0// fine_ge0//= lee_fin pmulrn_rge0//.
   by rewrite addr_gt0.
-apply; apply: ereal_sup_ub => /=.
+apply; apply: ereal_sup_ubound => /=.
 by exists (r + d)%R => //; rewrite in_itv/= andbT addr_gt0.
 Unshelve. all: by end_near. Qed.
 
@@ -6231,7 +6230,7 @@ have [r0|r0] := lerP r 0.
   by apply: HL_maximalT_ge0; split => //; exact: openT.
 rewrite muleDr//; last by rewrite ge0_adde_def// inE integral_ge0.
 rewrite leeD//.
-  by apply: ereal_sup_ub => /=; exists r => //; rewrite in_itv/= r0.
+  by apply: ereal_sup_ubound => /=; exists r => //; rewrite in_itv/= r0.
 under eq_integral do rewrite -(mule1 `| _ |).
 rewrite ge0_integralZl//; last exact: measurable_ball.
 rewrite integral_cst//; last exact: measurable_ball.
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index 0f9a8eb96..473f9ac80 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -1790,7 +1790,7 @@ have : {in D, (fun x => inf [set sups (h ^~ x) n | n in [set n | 0 <= n]%N])
 move/eq_measurable_fun; apply; apply: measurable_fun_infs => //.
   move=> t Dt; have [M hM] := f_lb _ Dt; exists M => _ [m /= nm <-].
   rewrite (@le_trans _ _ (h m t)) //; first by apply hM => /=; exists m.
-  by apply: sup_ub; [exact/has_ubound_sdrop/f_ub|exists m => /=].
+  by apply: sup_ubound; [exact/has_ubound_sdrop/f_ub|exists m => /=].
 by move=> k; exact: measurable_fun_sups.
 Qed.
 
@@ -2093,7 +2093,7 @@ have muU : mu U < mu D + eps%:E.
     by rewrite lee_nneseries.
   apply: le_lt_trans.
     by apply: epsilon_trick => //; rewrite divr_ge0// ltW.
-  rewrite {2}[eps]splitr EFinD addeA lte_le_add//.
+  rewrite {2}[eps]splitr EFinD addeA lte_leD//.
   rewrite (le_lt_trans _ zDe)// -sMz lee_nneseries// => i _.
   rewrite /= -wlength_Rhull wlength_itv !er_map_idfun.
   rewrite -lebesgue_measure_itv le_measure//= ?inE.
@@ -2197,7 +2197,7 @@ apply/lee_addgt0Pr => e e0.
 have [B [cB BA /= ABe]] := lebesgue_regularity_inner mA muA e0.
 rewrite -{1}(setDKU BA) (@le_trans _ _ (mu B + mu (A `\` B)))//.
   by rewrite setUC outer_measureU2.
-by rewrite leeD//; [apply: ereal_sup_ub => /=; exists B|exact/ltW].
+by rewrite leeD//; [apply: ereal_sup_ubound => /=; exists B|exact/ltW].
 Qed.
 
 Lemma lebesgue_regularity_inner_sup (D : set R) : measurable D ->
@@ -2222,7 +2222,7 @@ have [] := @lebesgue_regularity_inner (F N `&` D) _ _ _ ltr01.
 - by rewrite (le_lt_trans _ (ffin N).2)//= measureIl.
 move=> V [/[dup] /compact_measurable mV cptV VFND] FDV1 M1FD.
 rewrite (@le_trans _ _ (mu V))//; last first.
-  apply: ereal_sup_ub; exists V => //=; split => //.
+  apply: ereal_sup_ubound; exists V => //=; split => //.
   exact: (subset_trans VFND (@subIsetr _ _ _)).
 rewrite -(@leeD2rE _ 1)// -EFinD (le_trans M1FD)//.
 rewrite /mu (@measureDI _ _ _ _ (F N `&` D) _ _ mV)/=; last exact: measurableI.
diff --git a/theories/measure.v b/theories/measure.v
index 00cb507ff..e560b7617 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -4464,7 +4464,7 @@ Unshelve. all: by end_near. Qed.
 Lemma mu_ext0 : mu^* set0 = 0.
 Proof.
 apply/eqP; rewrite eq_le; apply/andP; split; last exact/mu_ext_ge0.
-rewrite /mu_ext; apply: ereal_inf_lb; exists (fun=> set0); first by split.
+rewrite /mu_ext; apply: ereal_inf_lbound; exists (fun=> set0); first by split.
 by apply: lim_near_cst => //; near=> n => /=; rewrite big1.
 Unshelve. all: by end_near. Qed.
 
@@ -4494,7 +4494,7 @@ have [G PG] : {G : ((set T)^nat)^nat & forall n, P n (G n)}.
     by move=> /= _ [B [mB AnB] <-]; exact: nneseries_ge0.
 have muG_ge0 x : 0 <= (mu \o uncurry G) x by exact: measure_ge0.
 apply: (@le_trans _ _ (\esum_(i in setT) (mu \o uncurry G) i)).
-  rewrite /mu_ext; apply: ereal_inf_lb => /=.
+  rewrite /mu_ext; apply: ereal_inf_lbound => /=.
   have /card_esym/ppcard_eqP[f] := card_nat2.
   exists (uncurry G \o f).
     split => [i|]; first exact/measurable_uncurry/(PG (f i).1).1.1.
@@ -4655,7 +4655,7 @@ Lemma measurable_mu_extE d (R : realType) (T : semiRingOfSetsType d)
   measurable X -> mu^* X = mu X.
 Proof.
 move=> mX; apply/eqP; rewrite eq_le; apply/andP; split.
-  apply: ereal_inf_lb; exists (fun n => if n is 0%N then X else set0).
+  apply: ereal_inf_lbound; exists (fun n => if n is 0%N then X else set0).
     by split=> [[]// _|t Xt]; exists 0%N.
   apply/cvg_lim => //; rewrite -cvg_shiftS.
   rewrite (_ : [sequence _]_n = cst (mu X)); first exact: cvg_cst.
@@ -4678,8 +4678,8 @@ Lemma Rmu_ext d (R : realType) (T : semiRingOfSetsType d)
   (measure mu)^* = mu^*.
 Proof.
 apply/funeqP => /= X; rewrite /mu_ext/=; apply/eqP; rewrite eq_le.
-rewrite ?lb_ereal_inf// => _ [F [Fm XS] <-]; rewrite ereal_inf_lb//; last first.
-  exists F; first by split=> // i; apply: sub_gen_smallest.
+rewrite ?lb_ereal_inf// => _ [F [Fm XS] <-]; rewrite ereal_inf_lbound//; last first.
+  exists F; first by split=> // i; exact: sub_gen_smallest.
   by rewrite (eq_eseriesr (fun _ _ => RmuE _ (Fm _))).
 pose K := [set: nat] `*`` fun i => decomp (F i).
 have /ppcard_eqP[f] : (K #= [set: nat])%card.
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 41f16dd13..8184ed7cc 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -3217,8 +3217,8 @@ rewrite -EFinD lee_fin -inf_sumE //; first last.
 apply: lb_le_inf.
   by exists (r1%:num + r2%:num); exists r1%:num => //; exists r2%:num.
 move=> ? [+ []] => _/posnumP[p] xpy [+ []] => _/posnumP[q] yqz <-.
-apply: inf_lb; first by exists 0 => ? /= [/ltW].
-by split => //; apply: (ball_triangle xpy).
+apply: inf_lbound; first by exists 0 => ? /= [/ltW].
+by split => //; exact: (ball_triangle xpy).
 Qed.
 
 Lemma edist_continuous : continuous edist.
@@ -3268,7 +3268,7 @@ have xxfin : edist (x, y) \is a fin_num.
 have dpose : fine (edist (x, y)) > 0 by rewrite -lte_fin fineK.
 pose eps := PosNum dpose.
 have : (edist (x, y) <= (eps%:num / 2)%:E)%E.
-  apply: ereal_inf_lb; exists (eps%:num / 2) => //; split => //.
+  apply: ereal_inf_lbound; exists (eps%:num / 2) => //; split => //.
   exact: (bxy (eps%:num / 2)%:pos).
 apply: contra_leP => _.
 by rewrite /= EFinM fineK// lte_pdivrMr// lte_pmulr// lte1n.
@@ -3312,7 +3312,8 @@ have [xyfin|] := boolP (edist (x, y) \is a fin_num); first last.
   by rewrite ge0_fin_numE// ?ltey // negbK => /eqP->; rewrite addye ?leey.
 apply/lee_addgt0Pr => _/posnumP[eps].
 have [//|? [a Aa <-] yaeps] := @lb_ereal_inf_adherent R _ eps%:num _ fyn.
-apply: le_trans; first by apply: (@ereal_inf_lb _ _ (edist (x, a))); exists a.
+apply: le_trans.
+  by apply: (@ereal_inf_lbound _ _ (edist (x, a))); exists a.
 apply: le_trans; first exact: (@edist_triangle _ _ _ y).
 by rewrite -addeA leeD2lE // ltW.
 Qed.
@@ -3361,7 +3362,7 @@ Unshelve. all: by end_near. Qed.
 Lemma edist_inf0 a : A a -> edist_inf a = 0%E.
 Proof.
 move=> Aa; apply: le_anti; apply/andP; split; last exact: edist_inf_ge0.
-by apply: ereal_inf_lb; exists a => //; exact: edist_refl.
+by apply: ereal_inf_lbound; exists a => //; exact: edist_refl.
 Qed.
 
 End edist_inf.
@@ -3397,7 +3398,7 @@ have [->|/set0P[a A0]] := eqVneq A set0.
   - by move=> ? [? ? <-].
 have dfin x : @edist_inf R T' A x \is a fin_num.
   rewrite ge0_fin_numE ?edist_inf_ge0 //; apply: le_lt_trans.
-    by apply: ereal_inf_lb; exists a.
+    by apply: ereal_inf_lbound; exists a.
   rewrite -ge0_fin_numE ?edist_ge0 //; apply/edist_finP => /=; exists 2 => //.
   exact: countable_uniform.countable_uniform_bounded.
 pose f' := (fun z => fine (@edist_inf R T' A z)) \min (fun=> eps%:num).
@@ -4475,13 +4476,13 @@ Lemma right_bounded_interior (R : realType) (X : set R) :
 Proof.
 move=> uX r Xr; rewrite /mkset ltNge; apply/negP.
 rewrite le_eqVlt => /orP[/eqP supXr|]; last first.
-  by apply/negP; rewrite -leNgt sup_ub //; exact: interior_subset.
+  by apply/negP; rewrite -leNgt sup_ubound//; exact: interior_subset.
 suff : ~ X^° (sup X) by rewrite supXr.
 case/nbhs_ballP => _/posnumP[e] supXeX.
 have [f XsupXf] : exists f : {posnum R}, X (sup X + f%:num).
   exists (e%:num / 2)%:pos; apply supXeX; rewrite /ball /= opprD addrA subrr.
   by rewrite sub0r normrN gtr0_norm // ltr_pdivrMr // ltr_pMr // ltr1n.
-have : sup X + f%:num <= sup X by apply sup_ub.
+have : sup X + f%:num <= sup X by exact: sup_ubound.
 by apply/negP; rewrite -ltNge; rewrite ltrDl.
 Qed.
 
@@ -4490,13 +4491,13 @@ Lemma left_bounded_interior (R : realType) (X : set R) :
 Proof.
 move=> lX r Xr; rewrite /mkset ltNge; apply/negP.
 rewrite le_eqVlt => /orP[/eqP rinfX|]; last first.
-  by apply/negP; rewrite -leNgt inf_lb //; exact: interior_subset.
+  by apply/negP; rewrite -leNgt inf_lbound//; exact: interior_subset.
 suff : ~ X^° (inf X) by rewrite -rinfX.
 case/nbhs_ballP => _/posnumP[e] supXeX.
 have [f XsupXf] : exists f : {posnum R}, X (inf X - f%:num).
   exists (e%:num / 2)%:pos; apply supXeX; rewrite /ball /= opprB addrCA subrr.
   by rewrite addr0 gtr0_norm // ltr_pdivrMr // ltr_pMr // ltr1n.
-have : inf X <= inf X - f%:num by apply inf_lb.
+have : inf X <= inf X - f%:num by exact: inf_lbound.
 by apply/negP; rewrite -ltNge; rewrite ltrBlDr ltrDl.
 Qed.
 
@@ -4569,11 +4570,11 @@ Proof.
 move=> x Xx/=; rewrite in_itv/=.
 case: (asboolP (has_lbound _)) => ?; case: (asboolP (has_ubound _)) => ? //=.
 + by case: asboolP => ?; case: asboolP => ? //=;
-     rewrite !(lteifF, lteifT, sup_ub, inf_lb, sup_ub_strict, inf_lb_strict).
+     rewrite !(lteifF,lteifT,sup_ubound,inf_lbound,sup_ub_strict,inf_lb_strict).
 + by case: asboolP => XinfX; rewrite !(lteifF, lteifT);
-     [rewrite inf_lb | rewrite inf_lb_strict].
+     [rewrite inf_lbound | rewrite inf_lb_strict].
 + by case: asboolP => XsupX; rewrite !(lteifF, lteifT);
-     [rewrite sup_ub | rewrite sup_ub_strict].
+     [rewrite sup_ubound | rewrite sup_ub_strict].
 Qed.
 
 Lemma is_intervalP (X : set R) : is_interval X <-> X = [set x | x \in Rhull X].
@@ -4643,7 +4644,7 @@ split => [cE x y Ex Ey z /andP[xz zy]|].
       by exists x; split => //; rewrite /mkset lexx /= (ltW xy).
     by move: sepA; rewrite /separated => -[] /disjoints_subset + _; apply.
   have /andP[xz zy] : x <= z < y.
-    rewrite sup_ub //=; [|by exists y => u [_] /andP[]|].
+    rewrite sup_ubound//=; [|by exists y => u [_] /andP[]|].
     + rewrite lt_neqAle sup_le_ub ?andbT; last by move=> u [_] /andP[].
       * by apply/negP; apply: contraPnot A1y => /eqP <-.
       * by exists x; split => //; rewrite /mkset /= lexx /= (ltW xy).
@@ -4674,7 +4675,7 @@ split => [cE x y Ex Ey z /andP[xz zy]|].
   have nA0z1 : ~ (A false) z1.
     move=> A0z1; have : z < z1 by rewrite /z1 ltrDl.
     apply/negP; rewrite -leNgt.
-     apply: sup_ub; first by exists y => u [_] /andP[].
+     apply: sup_ubound; first by exists y => u [_] /andP[].
     by split => //; rewrite /mkset /z1 (le_trans xz) /= ?lerDl // (ltW z1y).
   by rewrite EU => -[//|]; apply: contra_not ncA1z1; exact: subset_closure.
 Qed.
diff --git a/theories/real_interval.v b/theories/real_interval.v
index f9feec095..0577bc6ac 100644
--- a/theories/real_interval.v
+++ b/theories/real_interval.v
@@ -62,7 +62,7 @@ set s := sup _; apply/eqP; rewrite eq_le; apply/andP; split.
 - apply sup_le_ub; last by move=> ? /ltW.
   by exists (x - 1); rewrite !set_itvE/= ltrBlDr ltrDl.
 - rewrite leNgt; apply/negP => sx; pose p := (s + x) / 2.
-  suff /andP[?]: (p < x) && (s < p) by apply/negP; rewrite -leNgt sup_ub.
+  suff /andP[?]: (p < x) && (s < p) by apply/negP; rewrite -leNgt sup_ubound.
   by rewrite !midf_lt.
 Qed.
 
@@ -427,7 +427,7 @@ Proof.
 rewrite -subTset => x _ /=; exists `|(floor `|x| + 1)%R|%N => //=.
 rewrite in_itv/= !natr_absz intr_norm intrD.
 have : `|x| < `|(floor `|x|)%:~R + 1|.
-  by rewrite [ltRHS]ger0_norm ?intrD1 ?lt_succ_floor// ler0z addr_ge0// floor_ge0.
+  by rewrite [ltRHS]ger0_norm ?intrD1 ?lt_succ_floor// ler0z addr_ge0 ?floor_ge0.
 case: b => /=.
 - by move/ltW; rewrite ler_norml => /andP[-> ->].
 - by rewrite ltr_norml => /andP[-> /ltW->].
diff --git a/theories/realfun.v b/theories/realfun.v
index c3e8f3927..04a8e0fee 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -303,7 +303,7 @@ rewrite lerBlDr {}/M.
 move: b ab pb lef ubf => [[|] b|[//|]] ab pb lef ubf; set M := sup _ => Mefp.
 - near=> r; rewrite ler_distl; apply/andP; split.
   + suff: f r <= M by apply: le_trans; rewrite lerBlDr lerDl.
-    apply: sup_ub => //=; exists r => //; rewrite in_itv/=.
+    apply: sup_ubound => //=; exists r => //; rewrite in_itv/=.
     by apply/andP; split; near: r; [exact: nbhs_right_gt|exact: nbhs_right_lt].
   + rewrite (le_trans Mefp)// lerD2r lef//=; last 2 first.
       by rewrite in_itv/= ap.
@@ -311,7 +311,7 @@ move: b ab pb lef ubf => [[|] b|[//|]] ab pb lef ubf; set M := sup _ => Mefp.
     apply/andP; split; near: r; [exact: nbhs_right_gt|exact: nbhs_right_lt].
 - near=> r; rewrite ler_distl; apply/andP; split.
   + suff: f r <= M by apply: le_trans; rewrite lerBlDr lerDl.
-    apply: sup_ub => //=; exists r => //; rewrite in_itv/=.
+    apply: sup_ubound => //=; exists r => //; rewrite in_itv/=.
     by apply/andP; split; near: r; [exact: nbhs_right_gt|exact: nbhs_right_le].
   + rewrite (le_trans Mefp)// lerD2r lef//=; last 2 first.
       by rewrite in_itv/= ap.
@@ -319,7 +319,7 @@ move: b ab pb lef ubf => [[|] b|[//|]] ab pb lef ubf; set M := sup _ => Mefp.
     by apply/andP; split; near: r; [exact: nbhs_right_gt|exact: nbhs_right_le].
 - near=> r; rewrite ler_distl; apply/andP; split.
   suff: f r <= M by apply: le_trans; rewrite lerBlDr lerDl.
-  apply: sup_ub => //=; exists r => //; rewrite in_itv/= andbT.
+  apply: sup_ubound => //=; exists r => //; rewrite in_itv/= andbT.
     by near: r; apply: nbhs_right_gt.
   rewrite (le_trans Mefp)// lerD2r lef//.
   - by rewrite in_itv/= andbT; near: r; exact: nbhs_right_gt.
@@ -433,9 +433,9 @@ have <- : sup (range g) = fine l.
   apply: EFin_inj; rewrite -ereal_sup_EFin//; last 2 first.
     - exists (fine l) => /= _ [m _ <-]; rewrite /g /=.
       have [mx|xm] := ltP m x.
-        by rewrite fine_le// ?f_fin_num//; apply: ereal_sup_ub; exists x.
+        by rewrite fine_le// ?f_fin_num//; apply: ereal_sup_ubound; exists x.
       rewrite fine_le// ?f_fin_num//; first exact/xB.
-      by apply: ereal_sup_ub; exists m.
+      by apply: ereal_sup_ubound; exists m.
     - by exists (g 0%R), 0%R.
   rewrite fineK//; apply/eqP; rewrite eq_le; apply/andP; split.
     apply: le_ereal_sup => _ /= [_ [m _] <-] <-.
@@ -445,10 +445,10 @@ have <- : sup (range g) = fine l.
   apply: ub_ereal_sup => /= _ [m _] <-.
   have [mx|xm] := ltP m x.
     rewrite (le_trans (ndf _ _ (ltW mx)))//.
-    apply: ereal_sup_ub => /=; exists (fine (f x)); last first.
+    apply: ereal_sup_ubound => /=; exists (fine (f x)); last first.
       by rewrite fineK// f_fin_num.
     by exists m => //; rewrite /g mx.
-  apply: ereal_sup_ub => /=; exists (fine (f m)) => //.
+  apply: ereal_sup_ubound => /=; exists (fine (f m)) => //.
     by exists m => //; rewrite /g ltNge xm.
   by rewrite fineK ?f_fin_num//; exact: xB.
 suff: g x @[x --> +oo%R] --> sup (range g).
@@ -464,7 +464,7 @@ apply: nondecreasing_cvgr.
     * by apply: xB; rewrite (le_trans xm).
     * exact/ndf.
 - exists (fine l) => /= _ [m _ <-]; rewrite /g /=.
-  rewrite -lee_fin (fineK l_fin_num); apply: ereal_sup_ub.
+  rewrite -lee_fin (fineK l_fin_num); apply: ereal_sup_ubound.
   have [_|xm] := ltP m x; first by rewrite fineK// ?f_fin_num//; eexists.
   by rewrite fineK// ?f_fin_num//; [exists m|exact/xB].
 Unshelve. all: by end_near. Qed.
@@ -551,15 +551,15 @@ have <- : inf [set g x | x in [set` Interval (BRight a) b]] = fine l.
     - exists (fine l) => /= _ [m _ <-]; rewrite /g /=.
       case: ifPn => [/andP[am mx]|].
         rewrite fine_le// ?f_fin_num//; first by rewrite axA// am (ltW mx).
-        apply: ereal_inf_lb; exists m => //=.
+        apply: ereal_inf_lbound; exists m => //=.
         rewrite in_itv/= -[X in _ && X]/(BLeft m < b)%O am/=.
         by rewrite (le_lt_trans _ xb) ?ltW.
       rewrite negb_and -!leNgt => /orP[ma|xm].
         rewrite fine_le// ?f_fin_num ?inE//.
-        apply: ereal_inf_lb; exists x => //=.
+        apply: ereal_inf_lbound; exists x => //=.
         by rewrite in_itv/= -[X in _ && X]/(BLeft x < b)%O ax xb.
       rewrite fine_le// ?f_fin_num ?inE//.
-      apply: ereal_inf_lb; exists x => //=.
+      apply: ereal_inf_lbound; exists x => //=.
       by rewrite in_itv/= -[X in _ && X]/(BLeft x < b)%O ax xb.
     - rewrite {}/l in lnoo lpoo l_fin_num *.
       rewrite {}/S in Snoo lnoo lpoo l_fin_num *.
@@ -588,12 +588,12 @@ have <- : inf [set g x | x in [set` Interval (BRight a) b]] = fine l.
   apply: lb_ereal_inf => /= y [m] /=.
   rewrite in_itv/= -[X in _ && X]/(BLeft m < b)%O => /andP[am mb] <-{y}.
   have [mx|xm] := ltP m x.
-    apply: ereal_inf_lb => /=; exists (fine (f m)); last first.
+    apply: ereal_inf_lbound => /=; exists (fine (f m)); last first.
       by rewrite fineK// f_fin_num// axA// am (ltW mx).
     by exists m; [rewrite in_itv/= am|rewrite /g am mx].
   rewrite (@le_trans _ _ (f x))//; last first.
     by apply: ndf => //; rewrite in_itv//= ?ax ?am.
-  apply: ereal_inf_lb => /=; exists (fine (f x)); last first.
+  apply: ereal_inf_lbound => /=; exists (fine (f x)); last first.
     by rewrite fineK// f_fin_num ?inE.
   by exists x; [rewrite in_itv/= ax|rewrite /g ltxx andbF].
 suff: g x @[x --> a^'+] --> inf [set g x | x in [set` Interval (BRight a) b]].
@@ -627,7 +627,7 @@ apply: nondecreasing_at_right_cvgr => //.
   rewrite negb_and -!leNgt => /orP[|xm]; first by rewrite leNgt am.
   by rewrite (lt_le_trans am mn)/= ltNge (le_trans xm mn).
 - exists (fine l) => /= _ [m _ <-]; rewrite /g /=.
-  rewrite -lee_fin (fineK l_fin_num); apply: ereal_inf_lb.
+  rewrite -lee_fin (fineK l_fin_num); apply: ereal_inf_lbound.
   case: ifPn => [/andP[am mn0]|].
     rewrite fineK//; last by rewrite f_fin_num// axA// am (ltW mn0).
     exists m => //=.
@@ -693,7 +693,7 @@ Let sup_ball f a r := ereal_sup [set f x | x in ball a r `\ a].
 Let sup_ball_le f a r s : (r <= s)%R -> sup_ball f a r <= sup_ball f a s.
 Proof.
 move=> rs; apply: ub_ereal_sup => /= _ /= [t [rt ta] <-].
-by apply: ereal_sup_ub => /=; exists t => //; split => //; exact: le_ball rt.
+by apply: ereal_sup_ubound => /=; exists t => //; split => //; exact: le_ball rt.
 Qed.
 
 Let sup_ball_is_cvg f a : cvg (sup_ball f a e @[e --> 0^'+]).
@@ -726,13 +726,13 @@ move=> [e/= e0 fg].
 near=> r; apply: ub_ereal_sup => /= _ [s [pas /= /eqP ps]] <-.
 rewrite (@le_trans _ _ (g s))//.
   by rewrite (fg r)//= sub0r normrN gtr0_norm.
-by apply: ereal_sup_ub => /=; exists s => //; split => //; exact/eqP.
+by apply: ereal_sup_ubound => /=; exists s => //; split => //; exact/eqP.
 Unshelve. all: by end_near. Qed.
 
 Lemma lime_sup_lim f a : lime_sup f a = lim (sup_ball f a e @[e --> 0^'+]).
 Proof.
 apply/eqP; rewrite eq_le; apply/andP; split.
-  apply: lime_ge => //; near=> e; apply: ereal_inf_lb => /=.
+  apply: lime_ge => //; near=> e; apply: ereal_inf_lbound => /=.
   by exists (ball a e `\ a) => //=; exact: dnbhs_ball.
 apply: lb_ereal_inf => /= _ [A [r /= r0 arA] <-].
 apply: lime_le => //; near=> e.
@@ -792,7 +792,7 @@ apply: lee_lim => //.
 - apply: nondecreasing_at_right_is_cvge; near=> e => x y; rewrite !in_itv/=.
   by move=> /andP[? ?] /andP[? ?] xy; apply: leeD => //; exact: sup_ball_le.
 - near=> a0; apply: ub_ereal_sup => _ /= [a1 [a1ae a1a]] <-.
-  by apply: leeD; apply: ereal_sup_ub => /=; exists a1.
+  by apply: leeD; apply: ereal_sup_ubound => /=; exists a1.
 Unshelve. all: by end_near. Qed.
 
 Lemma lime_sup_le f g a :
@@ -811,7 +811,7 @@ have ? : exists2 x, ball a r x /\ x <> a & f x = f (a + r / 2)%R.
     rewrite /ball/= opprD addrA subrr sub0r normrN gtr0_norm ?divr_gt0//.
     by rewrite ltr_pdivrMr// ltr_pMr// ltr1n.
   by apply/eqP; rewrite gt_eqF// ltr_pwDr// divr_gt0.
-by exists (f (a + r / 2)) => //=; rewrite inf_ballE ereal_inf_lb.
+by exists (f (a + r / 2)) => //=; rewrite inf_ballE ereal_inf_lbound.
 Unshelve. all: by end_near. Qed.
 
 Local Lemma lim_lime_sup' f a l :
@@ -893,13 +893,13 @@ have H (e : {posnum R}) :
   rewrite negb_and => /orP[|].
     rewrite -ltNge => farl.
     have : ereal_inf [set sup_ball f a r | r in `]0%R, +oo[] < l%:E.
-      rewrite (le_lt_trans _ farl)//; apply: ereal_inf_lb => /=; exists r => //.
+      rewrite (le_lt_trans _ farl)//; apply: ereal_inf_lbound => /=; exists r => //.
       by rewrite in_itv/= r0.
     by rewrite fal ltxx.
   by rewrite -leNgt; apply: le_trans; rewrite leeD2r// fal.
 move=> e; have [d /andP[lfp fpe]] := H e.
 exists d => r /= [] prd rp.
-by rewrite (le_lt_trans _ fpe)//; apply: ereal_sup_ub => /=; exists r.
+by rewrite (le_lt_trans _ fpe)//; apply: ereal_sup_ubound => /=; exists r.
 Qed.
 
 Local Lemma lime_infP f a l :
@@ -950,7 +950,7 @@ rewrite /= ler_distlC; apply/andP; split.
   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 ge_min lexx.
-  apply: ereal_inf_lb => /=; exists (u n).
+  apply: ereal_inf_lbound => /=; exists (u n).
     split; last by apply/eqP; rewrite eq_sym lt_eqF.
     by apply: ucvg => //=; near: n; exists m.
   by rewrite fineK//; by near: n.
@@ -958,7 +958,7 @@ 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 ge_min lexx orbT.
-apply: ereal_sup_ub => /=; exists (u n).
+apply: ereal_sup_ubound => /=; exists (u n).
   split; last by apply/eqP; rewrite eq_sym lt_eqF.
   by apply: ucvg => //=; near: n; exists m.
 by rewrite fineK//; near: n.
@@ -2087,7 +2087,7 @@ Lemma total_variation_ge a b f : a <= b -> (`|f b - f a|%:E <= TV a b f)%E.
 Proof.
 rewrite le_eqVlt => /predU1P[<-{b}|ab].
   by rewrite total_variationxx subrr normr0.
-apply: ereal_sup_ub => /=; exists (variation a b f [:: b]).
+apply: ereal_sup_ubound => /=; exists (variation a b f [:: b]).
   exact/variations_variation/itv_partition1.
 by rewrite /variation/= big_nat_recr//= big_nil add0r.
 Qed.
@@ -2207,7 +2207,7 @@ rewrite [x in (_ + x)%E]ereal_sup_EFin //; last exact: variations_neq0.
 rewrite -EFinD -sup_sumE /has_sup; [|(by split => //; exact: variations_neq0)..].
 apply: ub_ereal_sup => ? [? [l pacl <- <-]]; rewrite lee_fin.
 apply: (le_trans (variation_itv_partitionLR _ ac _ _)) => //.
-apply: sup_ub => /=.
+apply: sup_ubound => /=.
   case: bdAB => M ubdM; case: bdAC => N ubdN; exists (N + M).
   move=> q [?] [i pabi <-] [? [j pbcj <-]] <-.
   by apply: lerD; [apply: ubdN;exists i|apply:ubdM;exists j].
@@ -2361,7 +2361,7 @@ move/lt_trans; apply.
 rewrite [in ltRHS](splitr (eps%:num)) EFinD lteD2rE// -addeA.
 apply: (@le_lt_trans _ _ (variation x t f (t :: nil))%:E).
   rewrite [in leRHS]variation_prev; last exact: itv_partition1.
-  rewrite geeDl// sube_le0; apply: ereal_sup_ub => /=.
+  rewrite geeDl// sube_le0; apply: ereal_sup_ubound => /=.
   exists (variation t b f (i :: j)) => //; apply: variations_variation.
   by rewrite /itv_partition/= ijb ij ti.
 by rewrite /variation/= big_nat_recr//= big_nil add0r distrC lte_fin.
diff --git a/theories/reals.v b/theories/reals.v
index 1e41479c7..a989068bb 100644
--- a/theories/reals.v
+++ b/theories/reals.v
@@ -259,7 +259,7 @@ Lemma sup0 : sup (@set0 R) = 0. Proof. exact: supremum0. Qed.
 
 Lemma sup1 x : sup [set x] = x. Proof. exact: supremum1. Qed.
 
-Lemma sup_ub {E} : has_ubound E -> ubound E (sup E).
+Lemma sup_ubound {E} : has_ubound E -> ubound E (sup E).
 Proof.
 move=> ubE; apply/ubP=> x x_in_E; move: (x) (x_in_E).
 by apply/ubP/sup_upper_bound=> //; split; first by exists x.
@@ -268,7 +268,7 @@ Qed.
 Lemma sup_ub_strict E : has_ubound E ->
   ~ E (sup E) -> E `<=` [set r | r < sup E].
 Proof.
-move=> ubE EsupE r Er; rewrite /mkset lt_neqAle sup_ub // andbT.
+move=> ubE EsupE r Er; rewrite /mkset lt_neqAle sup_ubound // andbT.
 by apply/negP => /eqP supEr; move: EsupE; rewrite -supEr.
 Qed.
 
@@ -300,9 +300,9 @@ Lemma sup_setU (A B : set R) : has_sup B ->
 Proof.
 move=> [B0 [l Bl]] AB; apply/eqP; rewrite eq_le; apply/andP; split.
 - apply sup_le_ub => [|x [Ax|]]; first by apply: subset_nonempty B0 => ?; right.
-  by case: B0 => b Bb; rewrite (le_trans (AB _ _ Ax Bb)) // sup_ub //; exists l.
-- by move=> Bx; rewrite sup_ub //; exists l.
-- apply sup_le_ub => // b Bb; apply sup_ub; last by right.
+  by case: B0 => b Bb; rewrite (le_trans (AB _ _ Ax Bb)) // sup_ubound //; exists l.
+- by move=> Bx; rewrite sup_ubound //; exists l.
+- apply sup_le_ub => // b Bb; apply: sup_ubound; last by right.
   by exists l => x [Ax|Bx]; [rewrite (le_trans (AB _ _ Ax Bb)) // Bl|exact: Bl].
 Qed.
 
@@ -314,6 +314,8 @@ by apply sup_le_ub => // y Sy; move: (g y) => -[// | /negP]; rewrite leNgt.
 Qed.
 
 End RealLemmas.
+#[deprecated(since="mathcomp-analysis 1.3.0", note="Renamed `sup_ubound`.")]
+Notation sup_ub := sup_ubound (only parsing).
 
 Section sup_sum.
 Context {R : realType}.
@@ -328,7 +330,7 @@ have ABsup : has_sup [set x + y | x in A & y in B].
   by apply: lerD; [exact: up | exact: uq].
 apply: le_anti; apply/andP; split.
   apply: sup_le_ub; first by case: ABsup.
-  by move=> ? [p Ap [q Bq] <-]; apply: lerD; exact: sup_ub.
+  by move=> ? [p Ap [q Bq] <-]; apply: lerD; exact: sup_ubound.
 rewrite leNgt -subr_gt0; apply/negP.
 set eps := (_ + _ - _) => epos.
 have e2pos : 0 < eps / 2%:R by rewrite divr_gt0// ltr0n.
@@ -384,13 +386,13 @@ Proof. by rewrite /inf image_set0 sup0 oppr0. Qed.
 Lemma inf1 x : inf [set x] = x.
 Proof. by rewrite /inf image_set1 sup1 opprK. Qed.
 
-Lemma inf_lb E : has_lbound E -> lbound E (inf E).
-Proof. by move/has_lb_ubN/sup_ub/ub_lbN; rewrite setNK. Qed.
+Lemma inf_lbound E : has_lbound E -> lbound E (inf E).
+Proof. by move/has_lb_ubN/sup_ubound/ub_lbN; rewrite setNK. Qed.
 
 Lemma inf_lb_strict E : has_lbound E ->
   ~ E (inf E) -> E `<=` [set r | inf E < r].
 Proof.
-move=> lE EinfE r Er; rewrite /mkset lt_neqAle inf_lb // andbT.
+move=> lE EinfE r Er; rewrite /mkset lt_neqAle inf_lbound // andbT.
 by apply/negP => /eqP infEr; move: EinfE; rewrite infEr.
 Qed.
 
@@ -422,6 +424,8 @@ by move=> <-; rewrite ltrNr opprK => r'x; exists r'.
 Qed.
 
 End InfTheory.
+#[deprecated(since="mathcomp-analysis 1.3.0", note="Renamed `inf_lbound`.")]
+Notation inf_lb := inf_lbound (only parsing).
 
 (* -------------------------------------------------------------------- *)
 Section FloorTheory.
@@ -641,7 +645,7 @@ Lemma lt_inf_imfset {T : Type} (F : T -> R) l :
 Proof.
 set P := [set y | _]; move=> hs; rewrite -subr_gt0.
 move=> /inf_adherent/(_ hs)[_ [x ->]]; rewrite addrCA subrr addr0 => ltFxl.
-by exists x => //; rewrite (inf_lb hs.2)//; exists x.
+by exists x => //; rewrite (inf_lbound hs.2)//; exists x.
 Qed.
 
 End Sup.
diff --git a/theories/sequences.v b/theories/sequences.v
index 703fae4aa..16fcdc52e 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -1539,21 +1539,21 @@ have <- : sup (range v_) = fine l.
   apply: EFin_inj; rewrite -ereal_sup_EFin//; last 2 first.
     - exists (fine l) => /= _ [m _ <-]; rewrite /v_ /= fine_le//.
         by rewrite u_fin_num// leq_addl.
-      by apply: ereal_sup_ub; exists (m + N)%N.
+      by apply: ereal_sup_ubound; exists (m + N)%N.
     - by exists (v_ 0%N), 0%N.
   rewrite fineK//; apply/eqP; rewrite eq_le; apply/andP; split.
     apply: le_ereal_sup => _ /= [_ [m _] <-] <-.
     by exists (m + N)%N => //; rewrite /v_/= fineK// u_fin_num// leq_addl.
   apply: ub_ereal_sup => /= _ [m _] <-.
   rewrite (@le_trans _ _ (u_ (m + N)%N))//; first by rewrite nd_u_// leq_addr.
-  apply: ereal_sup_ub => /=; exists (fine (u_ (m + N)%N)); first by exists m.
+  apply: ereal_sup_ubound => /=; exists (fine (u_ (m + N))); first by exists m.
   by rewrite fineK// u_fin_num// leq_addl.
 apply: nondecreasing_cvgn.
 - move=> m n mn /=; rewrite /v_ /= fine_le ?u_fin_num ?leq_addl//.
   by rewrite nd_u_// leq_add2r.
 - exists (fine l) => /= _ [m _ <-]; rewrite /v_ /= fine_le//.
     by rewrite u_fin_num// leq_addl.
-  by apply: ereal_sup_ub; exists (m + N)%N.
+  by apply: ereal_sup_ubound; exists (m + N).
 Unshelve. all: by end_near. Qed.
 
 Lemma ereal_nondecreasing_is_cvgn (R : realType) (u_ : (\bar R) ^nat) :
@@ -1654,7 +1654,7 @@ Lemma nneseries_lim_ge (R : realType) (u_ : (\bar R)^nat) (P : pred nat) k :
   \sum_(0 <= i < k | P i) u_ i <= \sum_(i <oo | P i) u_ i.
 Proof.
 move/ereal_nondecreasing_series/ereal_nondecreasing_cvgn/cvg_lim => -> //.
-by apply: ereal_sup_ub; exists k.
+by apply: ereal_sup_ubound; exists k.
 Qed.
 
 Lemma eseries_pinfty (R : realFieldType) (u_ : (\bar R)^nat)
@@ -2289,7 +2289,7 @@ apply: nonincreasing_is_cvgn.
   exact/nonincreasing_sups/bounded_fun_has_ubound/cvg_seq_bounded.
 exists (- (M + 1)) => _ [n _ <-]; rewrite (@le_trans _ _ (u n)) //.
   by apply/lerNnormlW/Mu => //; rewrite ltrDl.
-apply: sup_ub; last by exists n => /=.
+apply: sup_ubound; last by exists n => /=.
 exact/has_ubound_sdrop/bounded_fun_has_ubound/cvg_seq_bounded.
 Qed.
 
@@ -2302,7 +2302,7 @@ Lemma infs_le_sups u n : cvgn u -> infs u n <= sups u n.
 Proof.
 move=> cu; rewrite /infs /sups /=; set A := sdrop _ _.
 have [a Aa] : A !=set0 by exists (u n); rewrite /A /=; exists n => //=.
-rewrite (@le_trans _ _ a) //; [apply/inf_lb|apply/sup_ub] => //.
+rewrite (@le_trans _ _ a) //; [apply/inf_lbound|apply/sup_ubound] => //.
 - exact/has_lbound_sdrop/bounded_fun_has_lbound/cvg_seq_bounded.
 - exact/has_ubound_sdrop/bounded_fun_has_ubound/cvg_seq_bounded.
 Qed.
@@ -2313,7 +2313,7 @@ Proof.
 move=> u_ub u_lb; apply: nonincreasing_cvgn; first exact: nonincreasing_sups.
 case: u_lb => M uM; exists M => _ [n _ <-].
 rewrite (@le_trans _ _ (u n)) //; first by apply: uM; exists n.
-by apply: sup_ub; [exact/has_ubound_sdrop|exists n => /=].
+by apply: sup_ubound; [exact/has_ubound_sdrop|exists n => /=].
 Qed.
 
 Lemma cvg_infs_sup u : has_ubound (range u) -> has_lbound (range u) ->
@@ -2342,7 +2342,7 @@ move=> f_ub; rewrite predeqE => t; split.
   by rewrite /= in_itv /= rfmt.
 - move=> [Dt [k /= nk]]; rewrite in_itv /= andbT => rfkt.
   split=> //; rewrite /= in_itv /= andbT; apply: (lt_le_trans rfkt).
-  by apply: sup_ub; [exact/has_ubound_sdrop/f_ub|by exists k].
+  by apply: sup_ubound; [exact/has_ubound_sdrop/f_ub|by exists k].
 Qed.
 
 Lemma infs_preimage T (D : set T) r (f : (T -> R)^nat) n :
@@ -2357,7 +2357,7 @@ move=> lb_f; rewrite predeqE => t; split.
   by move=>  /(inf_lt h)[_ [m /= nm <-]] fmtr; split => //; exists m.
 - move=> [Dt [k /= nk]]; rewrite /= in_itv /= => fktr.
   rewrite in_itv /=; split => //; apply: le_lt_trans fktr.
-  by apply/inf_lb => //; [exact/has_lbound_sdrop/lb_f|by exists k].
+  by apply/inf_lbound => //; [exact/has_lbound_sdrop/lb_f|by exists k].
 Qed.
 
 Lemma bounded_fun_has_lbound_sups u :
@@ -2366,7 +2366,7 @@ Proof.
 move=> /[dup] ba /bounded_fun_has_lbound/has_lbound_sdrop h.
 have [M hM] := h O; exists M => y [n _ <-].
 rewrite (@le_trans _ _ (u n)) //; first by apply: hM; exists n.
-apply: sup_ub; last by exists n => /=.
+apply: sup_ubound; last by exists n => /=.
 by move: ba => /bounded_fun_has_ubound/has_ubound_sdrop; exact.
 Qed.
 
@@ -2376,7 +2376,7 @@ Proof.
 move=> /[dup] ba /bounded_fun_has_ubound/has_ubound_sdrop h.
 have [M hM] := h O; exists M => y [n _ <-].
 rewrite (@le_trans _ _ (u n)) //; last by apply: hM; exists n.
-apply: inf_lb; last by exists n => /=.
+apply: inf_lbound; last by exists n => /=.
 by move: ba => /bounded_fun_has_lbound/has_lbound_sdrop; exact.
 Qed.
 
@@ -2473,7 +2473,7 @@ Lemma le_limn_supD u v : bounded_fun u -> bounded_fun v ->
 Proof.
 move=> ba bb; have ab k : sups (u \+ v) k <= sups u k + sups v k.
   apply: sup_le_ub; first by exists ((u \+ v) k); exists k => /=.
-  by move=> M [n /= kn <-]; apply: lerD; apply: sup_ub; [
+  by move=> M [n /= kn <-]; apply: lerD; apply: sup_ubound; [
     exact/has_ubound_sdrop/bounded_fun_has_ubound; exact | exists n |
     exact/has_ubound_sdrop/bounded_fun_has_ubound; exact | exists n ].
 have cu : cvgn (sups u).
@@ -2495,7 +2495,7 @@ Lemma le_limn_infD u v : bounded_fun u -> bounded_fun v ->
 Proof.
 move=> ba bb; have ab k : infs u k + infs v k <= infs (u \+ v) k.
   apply: lb_le_inf; first by exists ((u \+ v) k); exists k => /=.
-  by move=> M [n /= kn <-]; apply: lerD; apply: inf_lb; [
+  by move=> M [n /= kn <-]; apply: lerD; apply: inf_lbound; [
     exact/has_lbound_sdrop/bounded_fun_has_lbound; exact | exists n |
     exact/has_lbound_sdrop/bounded_fun_has_lbound; exact | exists n ].
 have cu : cvgn (infs u).
@@ -2598,7 +2598,7 @@ Lemma einfs_le_esups u n : einfs u n <= esups u n.
 Proof.
 rewrite /einfs /=; set A := sdrop _ _; have [a Aa] : A !=set0.
   by exists (u n); rewrite /A /=; exists n => //=.
-by rewrite (@le_trans _ _ a) //; [exact/ereal_inf_lb|exact/ereal_sup_ub].
+by rewrite (@le_trans _ _ a)//; [exact/ereal_inf_lbound|exact/ereal_sup_ubound].
 Unshelve. all: by end_near. Qed.
 
 Lemma cvg_esups_inf u : esups u @ \oo --> ereal_inf (range (esups u)).
@@ -2621,7 +2621,7 @@ rewrite predeqE => t; split => /=.
   rewrite /= in_itv /= andbT=> /ereal_sup_gt[_ [/= k nk <-]] afnt.
   by exists k => //=; rewrite in_itv /= afnt.
 move=> -[k /= nk] /=; rewrite in_itv /= andbT => /lt_le_trans afkt.
-by rewrite in_itv andbT/=; apply/afkt/ereal_sup_ub; exists k.
+by rewrite in_itv andbT/=; apply/afkt/ereal_sup_ubound; exists k.
 Qed.
 
 Lemma einfs_preimage T (a : \bar R) (f : (T -> \bar R)^nat) n :
@@ -2630,7 +2630,7 @@ Lemma einfs_preimage T (a : \bar R) (f : (T -> \bar R)^nat) n :
 Proof.
 rewrite predeqE => t; split => /= [|h].
   rewrite in_itv andbT /= => h k nk /=.
-  by rewrite /= in_itv/= (le_trans h)//; apply: ereal_inf_lb; exists k.
+  by rewrite /= in_itv/= (le_trans h)//; apply: ereal_inf_lbound; exists k.
 rewrite /= in_itv /= andbT leNgt; apply/negP.
 move=> /ereal_inf_lt[_ /= [k nk <-]]; apply/negP.
 by have := h _ nk; rewrite /= in_itv /= andbT -leNgt.
@@ -2651,7 +2651,7 @@ Lemma limn_esup_lim u : limn_esup u = limn (esups u).
 Proof.
 apply/eqP; rewrite eq_le; apply/andP; split.
   apply: lime_ge; first exact: is_cvg_esups.
-  near=> m; apply: ereal_inf_lb => /=.
+  near=> m; apply: ereal_inf_lbound => /=.
   by exists [set k | (m <= k)%N] => //=; exists m.
 apply: lb_ereal_inf => /= _ [A [r /= r0 rA] <-].
 apply: lime_le; first exact: is_cvg_esups.
@@ -2686,17 +2686,17 @@ suff : einfs (fun n => l + u n) = (fun n => l + einfs u n) by move=> ->.
 rewrite funeqE => n.
 apply/eqP; rewrite eq_le; apply/andP; split.
 - rewrite addeC -leeBlDr//; apply: lb_ereal_inf => /= _ [m /= mn] <-.
-  rewrite leeBlDr//; apply: ereal_inf_lb.
+  rewrite leeBlDr//; apply: ereal_inf_lbound.
   by exists m => //; rewrite addeC.
 - apply: lb_ereal_inf => /= _ [m /= mn] <-.
-  by rewrite leeD2l//; apply: ereal_inf_lb; exists m => /=.
+  by rewrite leeD2l//; apply: ereal_inf_lbound; exists m => /=.
 Qed.
 
 Lemma limn_esup_le_cvg u l : limn_esup u <= l -> (forall n, l <= u n) ->
   u @ \oo --> l.
 Proof.
 move=> supul ul; have usupu n : l <= u n <= esups u n.
-  by rewrite ul /=; apply/ereal_sup_ub; exists n => /=.
+  by rewrite ul /=; apply/ereal_sup_ubound; exists n => /=.
 suff : esups u @ \oo --> l.
   by apply: (@squeeze_cvge _ _ _ _ (cst l)) => //; [exact: nearW|exact: cvg_cst].
 apply/cvg_closeP; split; first exact: is_cvg_esups.