diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 67bb43c3b6..5affd9f1be 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,12 +4,28 @@
 
 ### Added
 
+- in `constructive_ereal.v`:
+  + lemma `ltgte_fin_num`
+
 ### Changed
 
+- in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`:
+  + lemma `nondecreasing_right_continuousP` 
+  + definition `CumulativeBounded`
+
+- in `lebesgue_stieltjes_measure.v`, according to generalization of `Cumulative`, modified:
+  + lemmas `wlength_ge0`, `cumulative_content_sub_fsum`, `wlength_sigma_subadditive`, `lebesgue_stieltjes_measure_unique`
+  + definitions `lebesgue_stieltjes_measure`, `completed_lebesgue_stieltjes_measure`
+
 ### Renamed
 
 ### Generalized
 
+- in `lebesgue_stieltjes_measure.v` generalized (codomain is now an `orderNbhsType`):
+  + lemma `right_continuousW`
+  + record `isCumulative`
+  + definition `Cumulative`
+
 ### Deprecated
 
 ### Removed
diff --git a/classical/set_interval.v b/classical/set_interval.v
index 5cda86b556..2b9fce511a 100644
--- a/classical/set_interval.v
+++ b/classical/set_interval.v
@@ -20,9 +20,10 @@ From mathcomp Require Import functions.
 (*         factor a b x := (x - a) / (b - a)                                  *)
 (*             set_itvE == multirule to turn intervals into inequalities      *)
 (*     disjoint_itv i j == intervals i and j are disjoint                     *)
-(*         itv_is_ray i == i is either `]x,+oo[ or `]-oo,x[                   *)
-(*     itv_is_bd_open i == i is `]x,y[                                        *)
-(*      itv_open_ends i == i has open endpoints, E.G. is one of the two above *)
+(*         itv_is_ray i == i is either `]x, +oo[ or `]-oo, x[                 *)
+(*     itv_is_bd_open i == i is `]x, y[                                       *)
+(*      itv_open_ends i == i has open endpoints, i.e., it is one of the two   *)
+(*                         above                                              *)
 (*        is_open_itv A == the set A can be written as an open interval       *)
 (*     open_itv_cover A == the set A can be covered by open intervals         *)
 (* ```                                                                        *)
diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v
index 5fa11a3bbd..f48e46ca7b 100644
--- a/reals/constructive_ereal.v
+++ b/reals/constructive_ereal.v
@@ -1695,6 +1695,12 @@ Proof. by move: x => [x| |]//=; rewrite lee_fin => x0; rewrite ltNyr. Qed.
 Lemma lt0_fin_numE x : x < 0 -> (x \is a fin_num) = (-oo < x).
 Proof. by move/ltW; exact: le0_fin_numE. Qed.
 
+Lemma ltgte_fin_num x a b : a < x < b -> x \is a fin_num.
+Proof.
+rewrite fin_numE -ltey -ltNye.
+by move=> /andP[/(le_lt_trans (leNye _))->/=] /lt_le_trans -> //; exact: leey.
+Qed.
+
 Lemma eqyP x : x = +oo <-> (forall A, (0 < A)%R -> A%:E <= x).
 Proof.
 split=> [-> // A A0|Ax]; first by rewrite leey.
diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v
index 9a372846e7..c099013a8d 100644
--- a/theories/lebesgue_stieltjes_measure.v
+++ b/theories/lebesgue_stieltjes_measure.v
@@ -60,23 +60,24 @@ Reserved Notation "R .-ocitv.-measurable"
 Notation right_continuous f :=
   (forall x, f%function @ at_right x --> f%function x).
 
-Lemma right_continuousW (R : numFieldType) (f : R -> R) :
-  continuous f -> right_continuous f.
+Lemma right_continuousW (R : numFieldType) {d} (U : orderNbhsType d)
+  (f : R -> U) : continuous f -> right_continuous f.
 Proof. by move=> cf x; apply: cvg_within_filter; exact/cf. Qed.
 
-HB.mixin Record isCumulative (R : numFieldType) (f : R -> R) := {
-  cumulative_is_nondecreasing : {homo f : x y / x <= y} ;
+HB.mixin Record isCumulative (R : numFieldType) {d} (U : orderNbhsType d)
+  (f : R -> U) := {
+  cumulative_is_nondecreasing : nondecreasing f ;
   cumulative_is_right_continuous : right_continuous f }.
 
 #[short(type=cumulative)]
-HB.structure Definition Cumulative (R : numFieldType) :=
-  { f of isCumulative R f }.
+HB.structure Definition Cumulative
+  (R : numFieldType) {d} (U : orderNbhsType d) := { f of isCumulative R d U f }.
 
-Arguments cumulative_is_nondecreasing {R} _.
-Arguments cumulative_is_right_continuous {R} _.
+Arguments cumulative_is_nondecreasing {R d U} _.
+Arguments cumulative_is_right_continuous {R d U} _.
 
-Lemma nondecreasing_right_continuousP (R : numFieldType) (a : R) (e : R)
-    (f : cumulative R) :
+Lemma nondecreasing_right_continuousP (R : realFieldType) (a : R) (e : R)
+    (f : cumulative R R) :
   e > 0 -> exists d : {posnum R}, f (a + d%:num) <= f a + e.
 Proof.
 move=> e0; move: (cumulative_is_right_continuous f).
@@ -92,7 +93,7 @@ by rewrite opprB ltrBlDl => fa; exact: ltW.
 Qed.
 
 Section id_is_cumulative.
-Variable R : realType.
+Variable R : realFieldType.
 
 Let id_nd : {homo @idfun R : x y / x <= y}.
 Proof. by []. Qed.
@@ -100,7 +101,7 @@ Proof. by []. Qed.
 Let id_rc : right_continuous (@idfun R).
 Proof. by apply/right_continuousW => x; exact: cvg_id. Qed.
 
-HB.instance Definition _ := isCumulative.Build R idfun id_nd id_rc.
+HB.instance Definition _ := isCumulative.Build R _ R idfun id_nd id_rc.
 End id_is_cumulative.
 (* /TODO: move? *)
 
@@ -373,7 +374,7 @@ apply/andP; split=> //; apply: contraTneq xbj => ->.
 by rewrite in_itv/= le_gtF// (itvP xabi).
 Qed.
 
-Lemma wlength_ge0 (f : cumulative R) (I : set (ocitv_type R)) :
+Lemma wlength_ge0 (f : cumulative R R) (I : set (ocitv_type R)) :
   (0 <= wlength f I)%E.
 Proof.
 by rewrite -(wlength0 f) le_wlength//; exact: cumulative_is_nondecreasing.
@@ -381,14 +382,14 @@ Qed.
 
 #[local] Hint Extern 0 (0%:E <= wlength _ _) => solve[apply: wlength_ge0] : core.
 
-HB.instance Definition _ (f : cumulative R) :=
+HB.instance Definition _ (f : cumulative R R) :=
   isContent.Build _ _ R (wlength f)
     (wlength_ge0 f)
     (wlength_semi_additive f).
 
 Hint Extern 0 (measurable _) => solve [apply: is_ocitv] : core.
 
-Lemma cumulative_content_sub_fsum (f : cumulative R) (D : {fset nat}) a0 b0
+Lemma cumulative_content_sub_fsum (f : cumulative R R) (D : {fset nat}) a0 b0
     (a b : nat -> R) : (forall i, i \in D -> a i <= b i) ->
     `]a0, b0] `<=` \big[setU/set0]_(i <- D) `]a i, b i]%classic ->
   f b0 - f a0 <= \sum_(i <- D) (f (b i) - f (a i)).
@@ -406,7 +407,7 @@ rewrite -sumEFin fsbig_finite//= set_fsetK// big_seq [in leRHS]big_seq.
 by apply: lee_sum => i iD; rewrite wlength_itv_bnd// Dab.
 Qed.
 
-Lemma wlength_sigma_subadditive (f : cumulative R) :
+Lemma wlength_sigma_subadditive (f : cumulative R R) :
   measurable_subset_sigma_subadditive (wlength f).
 Proof.
 move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE => -[a _ <-].
@@ -475,7 +476,7 @@ rewrite big_seq [in X in (_ <= X)%E]big_seq; apply: lee_sum => k kX.
 by rewrite AE leeD2l// lee_fin lerBlDl natrX De.
 Qed.
 
-HB.instance Definition _ (f : cumulative R) :=
+HB.instance Definition _ (f : cumulative R R) :=
   Content_SigmaSubAdditive_isMeasure.Build _ _ _
     (wlength f) (wlength_sigma_subadditive f).
 
@@ -490,17 +491,18 @@ move=> k; split => //; rewrite wlength_itv /= -EFinB.
 by case: ifP; rewrite ltey.
 Qed.
 
-Definition lebesgue_stieltjes_measure (f : cumulative R) :=
+Definition lebesgue_stieltjes_measure (f : cumulative R R) :=
   measure_extension (wlength f).
-HB.instance Definition _ (f : cumulative R) :=
+HB.instance Definition _ (f : cumulative R R) :=
   Measure.on (lebesgue_stieltjes_measure f).
 
-Let sigmaT_finite_lebesgue_stieltjes_measure (f : cumulative R) :
+Let sigmaT_finite_lebesgue_stieltjes_measure (f : cumulative R R) :
   sigma_finite setT (lebesgue_stieltjes_measure f).
 Proof. exact/measure_extension_sigma_finite/wlength_sigma_finite. Qed.
 
-HB.instance Definition _ (f : cumulative R) := @Measure_isSigmaFinite.Build _ _ _
-  (lebesgue_stieltjes_measure f) (sigmaT_finite_lebesgue_stieltjes_measure f).
+HB.instance Definition _ (f : cumulative R R) :=
+  @Measure_isSigmaFinite.Build _ _ _ (lebesgue_stieltjes_measure f)
+    (sigmaT_finite_lebesgue_stieltjes_measure f).
 
 End wlength_extension.
 Arguments lebesgue_stieltjes_measure {R}.
@@ -512,7 +514,7 @@ Section lebesgue_stieltjes_measure.
 Variable R : realType.
 Let gitvs : measurableType _ := g_sigma_algebraType (@ocitv R).
 
-Lemma lebesgue_stieltjes_measure_unique (f : cumulative R)
+Lemma lebesgue_stieltjes_measure_unique (f : cumulative R R)
     (mu : {measure set gitvs -> \bar R}) :
     (forall X, ocitv X -> lebesgue_stieltjes_measure f X = mu X) ->
   forall X, measurable X -> lebesgue_stieltjes_measure f X = mu X.
@@ -527,17 +529,17 @@ End lebesgue_stieltjes_measure.
 Section completed_lebesgue_stieltjes_measure.
 Context {R : realType}.
 
-Definition completed_lebesgue_stieltjes_measure (f : cumulative R) :=
+Definition completed_lebesgue_stieltjes_measure (f : cumulative R R) :=
   @completed_measure_extension _ _ _ (wlength f).
 
-HB.instance Definition _ (f : cumulative R) :=
+HB.instance Definition _ (f : cumulative R R) :=
   Measure.on (@completed_lebesgue_stieltjes_measure f).
 
-Let sigmaT_finite_completed_lebesgue_stieltjes_measure (f : cumulative R) :
+Let sigmaT_finite_completed_lebesgue_stieltjes_measure (f : cumulative R R) :
   sigma_finite setT (@completed_lebesgue_stieltjes_measure f).
 Proof. exact/completed_measure_extension_sigma_finite/wlength_sigma_finite. Qed.
 
-HB.instance Definition _ (f : cumulative R) :=
+HB.instance Definition _ (f : cumulative R R) :=
   @Measure_isSigmaFinite.Build _ _ _
     (@completed_lebesgue_stieltjes_measure f)
     (sigmaT_finite_completed_lebesgue_stieltjes_measure f).
@@ -619,7 +621,7 @@ HB.mixin Record isCumulativeBounded (R : numFieldType) (l r : R) (f : R -> R) :=
   cumulativey : f @ +oo --> r }.
 
 #[short(type=cumulativeBounded)]
-HB.structure Definition CumulativeBounded (R : numFieldType) (l r : R) :=
+HB.structure Definition CumulativeBounded (R : realFieldType) (l r : R) :=
   { f of isCumulativeBounded R l r f & Cumulative R f}.
 
 Arguments cumulativeNy {R l r} s.
diff --git a/theories/normedtype_theory/ereal_normedtype.v b/theories/normedtype_theory/ereal_normedtype.v
index 016d59aad5..2225c83b02 100644
--- a/theories/normedtype_theory/ereal_normedtype.v
+++ b/theories/normedtype_theory/ereal_normedtype.v
@@ -482,3 +482,36 @@ split=> [|[Py]] [x [xr Px]]; last by exists x; split=> // -[y||]//; apply: Px.
 by split; [|exists x; split=> // y xy]; apply: Px.
 Qed.
 End nbhs_ereal.
+
+Section ereal_OrderNbhs.
+Variable R : realFieldType.
+
+Let ereal_order_nbhsE (x : \bar R) :
+  nbhs x = filter_from (fun i => itv_open_ends i /\ x \in i)
+                       (fun i => [set` i]).
+Proof.
+apply/seteqP; split=> A.
+- rewrite /nbhs/= /ereal_nbhs/=; move: x => [r [e/= e0 reA]||].
+  + exists `](r - e)%:E, (r + e)%:E[ => [|[y|/andP[]//|//]]; rewrite ?in_itv/=.
+    * by rewrite !lte_fin ltrBlDr andbb ltrDl; split => //; right.
+    * by move/subset_ball_prop_in_itv : reA => /(_ y); rewrite /= !in_itv.
+  + case=> M [Mreal MA].
+    exists `]M%:E, +oo[ => [|y/=]; rewrite in_itv/= andbT ?ltry; last exact: MA.
+    by split => //; left.
+  + case=> M [Mreal MA].
+    exists `]-oo, M%:E[ => [|y/=]; rewrite in_itv/= ?ltNyr; last exact: MA.
+    by split => //; left.
+- move=> [[ [[]/= r|[]] [[]/= s|[]] ]] [] []// _.
+  + move=> /[dup]/ltgte_fin_num/fineK <-; rewrite in_itv/=.
+    move=> /andP[rx sx] rsA; apply: (nbhs_interval rx sx) => z rz zs.
+    by apply: rsA =>/=; rewrite in_itv/= rz.
+  + rewrite nbhsE/= => rx rA; exists `]r, +oo[%classic => //.
+    by split => //; rewrite set_itvE; exact: open_ereal_gt_ereal.
+  + rewrite nbhsE/= => xs ?; exists `]-oo, s[%classic => //.
+    by split => //; rewrite set_itvE; exact: open_ereal_lt_ereal.
+  + by rewrite set_itvE/= subTset => _ ->; exact: filter_nbhsT.
+Qed.
+
+HB.instance Definition _ := Order_isNbhs.Build _ (\bar R) ereal_order_nbhsE.
+
+End ereal_OrderNbhs.
diff --git a/theories/probability.v b/theories/probability.v
index 0dc7b4f5a8..06fed1326a 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -247,6 +247,9 @@ have cdf_na : cdf X (a + n.+1%:R^-1) @[n --> \oo] --> cdf X a.
 by rewrite -(cvg_unique _ cdf_ns cdf_na).
 Unshelve. all: by end_near. Qed.
 
+HB.instance Definition _ := isCumulative.Build R _ (\bar R) (cdf X)
+  cdf_nondecreasing cdf_right_continuous.
+
 End cumulative_distribution_function.
 
 Section cdf_of_lebesgue_stieltjes_mesure.
diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v
index 28d54db18e..e265bb2eac 100644
--- a/theories/topology_theory/num_topology.v
+++ b/theories/topology_theory/num_topology.v
@@ -33,8 +33,7 @@ Variable (R : numDomainType).
 Lemma nbhs_filter (p : R^o) : ProperFilter (nbhs p).
 Proof.
 split.
-  move=> [] e e0 /subsetP/(_ p).
-  by rewrite !in_setE/= subrr normr0.
+  by move=> [] e e0 /subsetP/(_ p); rewrite !in_setE/= subrr normr0.
 split=> [|P Q|P Q].
 - by exists 1; [exact: ltr01|exact: subsetT].
 - move=> [] /= e e0 /subsetP eP [] /= f f0 /subsetP fQ.
@@ -89,9 +88,9 @@ Proof.
 rewrite eqEsubset; split => U.
   case => _ /posnumP[e] xeU.
   exists (`]x - e%:num, x + e%:num[); first split; first by right.
-    by rewrite in_itv /= -real_lter_distl subrr // normr0.
-  apply: (subset_trans _ xeU) => z /=.
-  by rewrite in_itv /= -real_lter_distl //= distrC.
+    by rewrite in_itv/= -lter_distl subrr normr0.
+  apply: subset_trans xeU => z /=.
+  by rewrite in_itv /= -lter_distl distrC.
 case => [][[[]l|[]]] [[]r|[]] [[]]//= _.
 - move=> xlr lrU; exists (Order.min (x - l) (r - x)).
     by rewrite /= lt_min ?lterBDr ?add0r ?(itvP xlr).
@@ -103,12 +102,12 @@ case => [][[[]l|[]]] [[]r|[]] [[]]//= _.
 - move=> xl lU; exists (x - l) => /=; first by rewrite lterBDr add0r (itvP xl).
   apply/(subset_trans _ lU)/subset_ball_prop_in_itv.
   suff : (`]x - (x - l), x + (x - l)[ <= `]l, +oo[)%O.
-    by move/subitvP => H ?; exact: H.
+    by move/subitvP => + ?; exact.
   by rewrite subitvE lteBSide/= subKr lexx.
 - move=> xr rU; exists (r - x) => /=; first by rewrite lterBDr add0r (itvP xr).
   apply/(subset_trans _ rU)/subset_ball_prop_in_itv.
   suff : (`]x - (r - x), x + (r - x)[ <= `]-oo, r[)%O.
-    by move/subitvP => H ?; exact: H.
+    by move/subitvP => + ?; exact.
   by rewrite subitvE lteBSide/= addrC subrK.
 - by move=> _; rewrite set_itvE subTset => ->; exists 1 => /=.
 Qed.
@@ -131,12 +130,16 @@ HB.instance Definition _ (R : realFieldType) := PseudoPointedMetric.copy R R^o.
 HB.instance Definition _ (R : numClosedFieldType) :=
   PseudoPointedMetric.copy R R^o.
 
+#[export, non_forgetful_inheritance]
+HB.instance Definition _ (R : numFieldType) := PseudoPointedMetric.copy R R^o.
+
 #[export, non_forgetful_inheritance]
 HB.instance Definition _ (R : realFieldType) :=
   Order_isNbhs.Build _ R (@real_order_nbhsE R).
 
 #[export, non_forgetful_inheritance]
-HB.instance Definition _ (R : numFieldType) := PseudoPointedMetric.copy R R^o.
+HB.instance Definition _ (R : realType) :=
+  Order_isNbhs.Build _ R (@real_order_nbhsE R).
 
 Module Exports. HB.reexport. End Exports.