diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index a487b863a..df2f0239e 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -14,6 +14,26 @@
 - in `measure.v`:
   + lemmas `negligibleI`, `negligible_bigsetU`, `negligible_bigcup`
 
+- in `reals.v`:
+  + lemma `le_inf`
+- in `constructive_ereal.v`:
+  + lemmas `le_er_map`, `er_map_idfun`
+- new `lebesgue_stieltjes_measure.v`:
+  + notation `right_continuous`
+  + lemmas `right_continuousW`, `nondecreasing_right_continuousP`
+  + mixin `isCumulative`, structure `Cumulative`, notation `cumulative`
+  + `idfun` instance of `Cumulative`
+  + `wlength`, `wlength0`, `wlength_singleton`, `wlength_setT`, `wlength_itv`,
+    `wlength_finite_fin_num`, `finite_wlength_itv`, `wlength_itv_bnd`, `wlength_infty_bnd`,
+    `wlength_bnd_infty`, `infinite_wlength_itv`, `wlength_itv_ge0`, `wlength_Rhull`,
+    `le_wlength_itv`, `le_wlength`, `wlength_semi_additive`, `wlength_ge0`,
+    `lebesgue_stieltjes_measure_unique`
+  + content instance of `hlength`
+  + `cumulative_content_sub_fsum`,
+    `wlength_sigma_sub_additive`, `wlength_sigma_finite`
+  + measure instance of `hlength`
+  + definition `lebesgue_stieltjes_measure`
+
 ### Changed
 
 - in `hoelder.v`:
@@ -25,11 +45,30 @@
   + order of parameters changed in `semi_sigma_additive_is_additive`,
     `isMeasure`
 
+- in `lebesgue_measure.v`:
+  + are now prefixed with `LebesgueMeasure`:
+    * `hlength`, `hlength0`, `hlength_singleton`, `hlength_setT`, `hlength_itv`,
+      `hlength_finite_fin_num`, `hlength_infty_bnd`,
+      `hlength_bnd_infty`, `hlength_itv_ge0`, `hlength_Rhull`,
+      `le_hlength_itv`, `le_hlength`, `hlength_ge0`, `hlength_semi_additive`,
+      `hlength_sigma_sub_additive`, `hlength_sigma_finite`, `lebesgue_measure`
+    * `finite_hlengthE` renamed to `finite_hlentgh_itv`
+    * `pinfty_hlength` renamed to `infinite_hlength_itv`
+  + `lebesgue_measure` now defined with `lebesgue_stieltjes_measure`
+  + `lebesgue_measure_itv` does not refer to `hlength` anymore
+- moved from `lebesgue_measure.v` to `lebesgue_stieltjes_measure.v`
+  + notations `_.-ocitv`, `_.-ocitv.-measurable`
+  + definitions `ocitv`, `ocitv_display`
+  + lemmas `is_ocitv`, `ocitv0`, `ocitvP`, `ocitvD`, `ocitvI`
+
 ### Renamed
 
 - in `charge.v`
   + `isCharge` -> `isSemiSigmaAdditive`
 
+- in `ereal.v`:
+  + `le_er_map` -> `le_er_map_in`
+
 ### Generalized
 
 - in `topology.v`:
@@ -39,6 +78,8 @@
 
 ### Removed
 
+- `lebesgue_measure_unique` (generalized to `lebesgue_stieltjes_measure_unique`)
+
 ### Infrastructure
 
 ### Misc
diff --git a/_CoqProject b/_CoqProject
index 9521968f4..fb6175469 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -32,6 +32,7 @@ theories/nsatz_realtype.v
 theories/esum.v
 theories/real_interval.v
 theories/lebesgue_measure.v
+theories/lebesgue_stieltjes_measure.v
 theories/forms.v
 theories/derive.v
 theories/measure.v
diff --git a/theories/Make b/theories/Make
index cd6285c45..4cf4ff2c6 100644
--- a/theories/Make
+++ b/theories/Make
@@ -30,6 +30,7 @@ numfun.v
 lebesgue_integral.v
 hoelder.v
 probability.v
+lebesgue_stieltjes_measure.v
 summability.v
 signed.v
 itv.v
diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v
index 9f099adac..b146d568d 100644
--- a/theories/constructive_ereal.v
+++ b/theories/constructive_ereal.v
@@ -123,6 +123,9 @@ Definition er_map T T' (f : T -> T') (x : \bar T) : \bar T' :=
   | -oo => -oo
   end.
 
+Lemma er_map_idfun T (x : \bar T) : er_map idfun x = x.
+Proof. by case: x. Qed.
+
 Definition fine {R : zmodType} x : R := if x is EFin v then v else 0.
 
 Section EqEReal.
@@ -356,6 +359,13 @@ Definition lteey := (ltey, leey).
 
 Definition lteNye := (ltNye, leNye).
 
+Lemma le_er_map (f : R -> R) : {homo f : x y / (x <= y)%R} ->
+  {homo er_map f : x y / x <= y}.
+Proof.
+move=> ndf.
+by move=> [r| |] [l| |]//=; rewrite ?leey ?leNye// !lee_fin; exact: ndf.
+Qed.
+
 Lemma le_total_ereal : totalPOrderMixin [porderType of \bar R].
 Proof.
 by move=> [?||][?||]//=; rewrite (ltEereal, leEereal)/= ?num_real ?le_total.
diff --git a/theories/ereal.v b/theories/ereal.v
index de97ccc88..a249452e7 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -162,7 +162,7 @@ Section ERealArithTh_realDomainType.
 Context {R : realDomainType}.
 Implicit Types (x y z u a b : \bar R) (r : R).
 
-Lemma le_er_map (A : set R) (f : R -> R) :
+Lemma le_er_map_in (A : set R) (f : R -> R) :
   {in A &, {homo f : x y / (x <= y)%O}} ->
   {in (EFin @` A)%classic &, {homo er_map f : x y / (x <= y)%E}}.
 Proof.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 57107fe01..40517b53e 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -4869,7 +4869,7 @@ move=> /[dup]/compact_measurable => mA /compact_bounded[N [_ N1x]].
 have AN1 : (A `<=` `[- (`|N| + 1), `|N| + 1])%R.
   by move=> z Az; rewrite set_itvcc /= -ler_norml N1x// ltr_spaddr// ler_norm.
 rewrite (le_lt_trans (le_measure _ _ _ AN1)) ?inE//=.
-by rewrite lebesgue_measure_itv hlength_itv/= lte_fin gtr_opp// EFinD ltry.
+by rewrite lebesgue_measure_itv/= lte_fin gtr_opp// EFinD ltry.
 Qed.
 
 Lemma continuous_compact_integrable (f : R -> R^o) (A : set R^o) :
@@ -5571,7 +5571,7 @@ have ball_itv2 r : 0 < r -> ball x r = `[x - r, x + r] `\` [set x + r; x - r].
   rewrite -ball_itvr // setDD setIC; apply/esym/setIidPl.
   by rewrite ballE set_itvcc => ?/=; rewrite in_itv => /andP [/ltW -> /ltW ->].
 have ritv r : 0 < r -> mu `[x - r, x + r]%classic = (r *+ 2)%:E.
-  move=> /gt0_cp rE; rewrite /= lebesgue_measure_itv hlength_itv /= lte_fin.
+  move=> /gt0_cp rE; rewrite /= lebesgue_measure_itv/= lte_fin.
   rewrite ler_lt_add // ?rE // -EFinD; congr (_ _).
   by rewrite opprB addrAC [_ - _]addrC addrA subrr add0r.
 move=> oA intf ctsfx Ax.
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index 714117b0c..530af5039 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -6,23 +6,20 @@ From mathcomp Require Import cardinality fsbigop.
 Require Import reals ereal signed topology numfun normedtype.
 From HB Require Import structures.
 Require Import sequences esum measure real_interval realfun exp.
+Require Export lebesgue_stieltjes_measure.
 
 (******************************************************************************)
 (*                            Lebesgue Measure                                *)
 (*                                                                            *)
 (* This file contains a formalization of the Lebesgue measure using the       *)
-(* Caratheodory's theorem available in measure.v and further develops the     *)
-(* theory of measurable functions.                                            *)
+(* Measure Extension theorem from measure.v and further develops the theory   *)
+(* of measurable functions.                                                   *)
 (*                                                                            *)
 (* Main reference:                                                            *)
 (* - Daniel Li, Intégration et applications, 2016                             *)
 (* - Achim Klenke, Probability Theory 2nd edition, 2014                       *)
 (*                                                                            *)
-(*             hlength A == length of the hull of the set of real numbers A   *)
-(*                 ocitv == set of open-closed intervals ]x, y] where         *)
-(*                            x and y are real numbers                        *)
 (*      lebesgue_measure == the Lebesgue measure                              *)
-(*                                                                            *)
 (*              ps_infty == inductive definition of the powerset              *)
 (*                          {0, {-oo}, {+oo}, {-oo,+oo}}                      *)
 (*         emeasurable G == sigma-algebra over \bar R built out of the        *)
@@ -49,82 +46,17 @@ Import numFieldTopology.Exports.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
-Reserved Notation "R .-ocitv" (at level 1, format "R .-ocitv").
-Reserved Notation "R .-ocitv.-measurable"
- (at level 2, format "R .-ocitv.-measurable").
-
-Section itv_semiRingOfSets.
-Variable R : realType.
-Implicit Types (I J K : set R).
-Definition ocitv_type : Type := R.
-
-Definition ocitv := [set `]x.1, x.2]%classic | x in [set: R * R]].
-
-Lemma is_ocitv a b : ocitv `]a, b]%classic.
-Proof. by exists (a, b); split => //=; rewrite in_itv/= andbT. Qed.
-Hint Extern 0 (ocitv _) => solve [apply: is_ocitv] : core.
-
-Lemma ocitv0 : ocitv set0.
-Proof. by exists (1, 0); rewrite //= set_itv_ge ?bnd_simp//= ltr10. Qed.
-Hint Resolve ocitv0 : core.
-
-Lemma ocitvP X : ocitv X <-> X = set0 \/ exists2 x, x.1 < x.2 & X = `]x.1, x.2]%classic.
-Proof.
-split=> [[x _ <-]|[->//|[x xlt ->]]]//.
-case: (boolP (x.1 < x.2)) => x12; first by right; exists x.
-by left; rewrite set_itv_ge.
-Qed.
-
-Lemma ocitvD : semi_setD_closed ocitv.
-Proof.
-move=> _ _ [a _ <-] /ocitvP[|[b ltb]] ->.
-  rewrite setD0; exists [set `]a.1, a.2]%classic].
-  by split=> [//|? ->//||? ? -> ->//]; rewrite bigcup_set1.
-rewrite setDE setCitv/= setIUr -!set_itvI.
-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 /= [].
-  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 /=.
-  move=> /andP[a1x xb1] /andP[b2x xa2].
-  by have := lt_le_trans b2x xb1; case: ltgtP ltb.
-exists ((if a.1 < c then [set `]a.1, c]%classic] else set0) `|`
-        (if d < a.2 then [set `]d, a.2]%classic] else set0)); split.
-- by rewrite finite_setU; do! case: ifP.
-- by move=> ? []; case: ifP => ? // ->//=.
-- by rewrite bigcup_setU; congr (_ `|` _);
-     case: ifPn => ?; rewrite ?bigcup_set1 ?bigcup_set0// set_itv_ge.
-- move=> I J/=; case: ifP => //= ac; case: ifP => //= da [] // -> []// ->.
-    by rewrite inside// => -[].
-  by rewrite setIC inside// => -[].
-Qed.
-
-Lemma ocitvI : setI_closed ocitv.
-Proof.
-move=> _ _ [a _ <-] [b _ <-]; rewrite -set_itvI/=.
-rewrite /Order.meet/= /Order.meet /Order.join/=
-        ?(andbF, orbF)/= ?(meetEtotal, joinEtotal).
-by rewrite -negb_or le_total/=.
-Qed.
-
-Definition ocitv_display : Type -> measure_display. Proof. exact. Qed.
-
-HB.instance Definition _ :=
-  @isSemiRingOfSets.Build (ocitv_display R)
-    ocitv_type (Pointed.class R) ocitv ocitv0 ocitvI ocitvD.
-
-Notation "R .-ocitv" := (ocitv_display R) : measure_display_scope.
-Notation "R .-ocitv.-measurable" := (measurable : set (set (ocitv_type))) :
-  classical_set_scope.
-
+(* This module contains a direct construction of the Lebesgue measure that is
+   kept here for archival purpose. The Lebesgue measure is actually defined as
+   an instance of the Lebesgue-Stieltjes measure. *)
+Module LebesgueMeasure.
 Section hlength.
+Context {R : realType}.
 Local Open Scope ereal_scope.
 Implicit Types i j : interval R.
 
-Definition hlength (A : set ocitv_type) : \bar R := let i := Rhull A in i.2 - i.1.
+Definition hlength (A : set (ocitv_type R)) : \bar R :=
+  let i := Rhull A in i.2 - i.1.
 
 Lemma hlength0 : hlength (set0 : set R) = 0.
 Proof. by rewrite /hlength Rhull0 /= subee. Qed.
@@ -161,7 +93,7 @@ by move=> _; rewrite hlength_itv /= ltNyr.
 by move=> _; rewrite hlength_itv.
 Qed.
 
-Lemma finite_hlengthE i : neitv i -> hlength [set` i] < +oo ->
+Lemma finite_hlength_itv i : neitv i -> hlength [set` i] < +oo ->
   hlength [set` i] = (fine i.2)%:E - (fine i.1)%:E.
 Proof.
 move=> i0 ioo; have [ri1 ri2] := hlength_finite_fin_num i0 ioo.
@@ -178,7 +110,7 @@ Lemma hlength_bnd_infty b r :
   hlength [set` Interval (BSide b r) +oo%O] = +oo :> \bar R.
 Proof. by rewrite hlength_itv /= ltry. Qed.
 
-Lemma pinfty_hlength i : hlength [set` i] = +oo ->
+Lemma infinite_hlength_itv i : hlength [set` i] = +oo ->
   (exists s r, i = Interval -oo%O (BSide s r) \/ i = Interval (BSide s r) +oo%O)
   \/ i = `]-oo, +oo[.
 Proof.
@@ -263,6 +195,11 @@ End hlength.
 (* by rewrite lt_geF ?midf_lt//= andbF le_gtF ?midf_le//= ltW. *)
 (* Qed. *)
 
+Section hlength_extension.
+Context {R : realType}.
+
+Notation hlength := (@hlength R).
+
 Lemma hlength_semi_additive : semi_additive hlength.
 Proof.
 move=> /= I n /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym-/funext {I}->.
@@ -334,7 +271,7 @@ HB.instance Definition _ := isContent.Build _ _ R
 Hint Extern 0 ((_ .-ocitv).-measurable _) => solve [apply: is_ocitv] : core.
 
 Lemma hlength_sigma_sub_additive :
-  sigma_sub_additive (hlength : set ocitv_type -> _).
+  sigma_sub_additive (hlength : set (ocitv_type R) -> _).
 Proof.
 move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE.
 move=> [a _ <-]; rewrite hlength_itv ?lte_fin/= -EFinB => lebig.
@@ -345,9 +282,9 @@ apply: le_trans (epsilon_trick _ _ _) => //=.
 have eVn_gt0 n : 0 < e%:num / 2 / (2 ^ n.+1)%:R.
   by rewrite divr_gt0// ltr0n// expn_gt0.
 have eVn_ge0 n := ltW (eVn_gt0 n).
-pose Aoo i : set ocitv_type :=
+pose Aoo i : set (ocitv_type R) :=
   `](b i).1, (b i).2 + e%:num / 2 / (2 ^ i.+1)%:R[%classic.
-pose Aoc i : set ocitv_type :=
+pose Aoc i : set (ocitv_type R) :=
   `](b i).1, (b i).2 + e%:num / 2 / (2 ^ i.+1)%:R]%classic.
 have: `[a.1 + e%:num / 2, a.2] `<=` \bigcup_i Aoo i.
   apply: (@subset_trans _ `]a.1, a.2]).
@@ -362,7 +299,7 @@ have: `](a.1 + e%:num / 2), a.2] `<=` \bigcup_(i in [set` X]) Aoc i.
   move=> x /subset_itv_oc_cc /Xc [i /= Xi] Aooix.
   by exists i => //; apply: subset_itv_oo_oc Aooix.
 have /[apply] := @content_sub_fsum _ _ _
-  [the content _ _ of hlength : set ocitv_type -> _] _ [set` X].
+  [the content _ _ of hlength : set (ocitv_type R) -> _] _ [set` X].
 move=> /(_ _ _ _)/Box[]//=; apply: le_le_trans.
   rewrite hlength_itv ?lte_fin -?EFinD/= -addrA -opprD.
   by case: ltP => //; rewrite lee_fin subr_le0.
@@ -378,7 +315,7 @@ Qed.
 HB.instance Definition _ := Content_SubSigmaAdditive_isMeasure.Build _ _ _
   hlength hlength_sigma_sub_additive.
 
-Lemma hlength_sigma_finite : sigma_finite setT (hlength : set ocitv_type -> _).
+Lemma hlength_sigma_finite : sigma_finite setT (hlength : set (ocitv_type R) -> _).
 Proof.
 exists (fun k : nat => `] (- k%:R)%R, k%:R]%classic); first by rewrite bigcup_itvT.
 by move=> k; split => //; rewrite hlength_itv/= -EFinB; case: ifP; rewrite ltry.
@@ -387,36 +324,23 @@ Qed.
 Definition lebesgue_measure := measure_extension [the measure _ _ of hlength].
 HB.instance Definition _ := Measure.on lebesgue_measure.
 
-(* TODO: this ought to be turned into a Let but older version of mathcomp/coq
-   does not seem to allow, try to change asap *)
-Local Lemma sigmaT_finite_lebesgue_measure : sigma_finite setT lebesgue_measure.
+Let sigmaT_finite_lebesgue_measure : sigma_finite setT lebesgue_measure.
 Proof. exact/measure_extension_sigma_finite/hlength_sigma_finite. Qed.
 
 HB.instance Definition _ := @isSigmaFinite.Build _ _ _
   lebesgue_measure sigmaT_finite_lebesgue_measure.
 
-End itv_semiRingOfSets.
-Arguments hlength {R}.
-#[global] Hint Extern 0 (0%:E <= hlength _) => solve[apply: hlength_ge0] : core.
-Arguments lebesgue_measure {R}.
+End hlength_extension.
 
-Notation "R .-ocitv" := (ocitv_display R) : measure_display_scope.
-Notation "R .-ocitv.-measurable" := (measurable : set (set (ocitv_type R))) :
-  classical_set_scope.
+End LebesgueMeasure.
 
-Section lebesgue_measure.
-Variable R : realType.
-Let gitvs := [the measurableType _ of salgebraType (@ocitv R)].
-
-Lemma lebesgue_measure_unique (mu : {measure set gitvs -> \bar R}) :
-  (forall X, ocitv X -> hlength X = mu X) ->
-  forall X, measurable X -> lebesgue_measure X = mu X.
-Proof.
-move=> muE X mX; apply: measure_extension_unique => //.
-exact: hlength_sigma_finite.
-Qed.
-
-End lebesgue_measure.
+Definition lebesgue_measure {R : realType} :
+  set [the measurableType _.-sigma of
+       salgebraType R.-ocitv.-measurable] -> \bar R :=
+  [the measure _ _ of lebesgue_stieltjes_measure [the cumulative _ of idfun]].
+HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R).
+HB.instance Definition _ (R : realType) :=
+  SigmaFiniteContent.on (@lebesgue_measure R).
 
 Section ps_infty.
 Context {T : Type}.
@@ -799,10 +723,11 @@ Section lebesgue_measure_itv.
 Variable R : realType.
 
 Let lebesgue_measure_itvoc (a b : R) :
-  (lebesgue_measure (`]a, b] : set R) = hlength `]a, b])%classic.
+  (lebesgue_measure (`]a, b] : set R) =
+  wlength [the cumulative _ of idfun] `]a, b])%classic.
 Proof.
-rewrite /lebesgue_measure/= /measure_extension measurable_mu_extE//.
-by exists (a, b).
+rewrite /lebesgue_measure/= /lebesgue_stieltjes_measure/= /measure_extension/=.
+by rewrite measurable_mu_extE//; exact: is_ocitv.
 Qed.
 
 Let lebesgue_measure_itvoo_subr1 (a : R) :
@@ -819,7 +744,7 @@ rewrite itv_bnd_open_bigcup//; transitivity (lim (lebesgue_measure \o
 rewrite (_ : _ \o _ = (fun n => (1 - n.+1%:R^-1)%:E)); last first.
   apply/funext => n /=; rewrite lebesgue_measure_itvoc.
   have [->|n0] := eqVneq n 0%N; first by rewrite invr1 subrr set_itvoc0.
-  rewrite hlength_itv/= lte_fin ifT; last first.
+  rewrite wlength_itv/= lte_fin ifT; last first.
     by rewrite ler_lt_sub// invr_lt1 ?unitfE// ltr1n ltnS lt0n.
   by rewrite !(EFinB,EFinN) fin_num_oppeB// addeAC addeA subee// add0e.
 apply/cvg_lim => //=; apply/fine_cvgP; split => /=; first exact: nearW.
@@ -834,47 +759,50 @@ suff : (lebesgue_measure (`]a - 1, a]%classic%R : set R) =
         lebesgue_measure (`]a - 1, a[%classic%R : set R) +
         lebesgue_measure [set a])%E.
   rewrite lebesgue_measure_itvoo_subr1 lebesgue_measure_itvoc => /eqP.
-  rewrite hlength_itv lte_fin ltr_subl_addr ltr_addl ltr01.
+  rewrite wlength_itv lte_fin ltr_subl_addr ltr_addl ltr01.
   rewrite [in X in X == _]/= EFinN EFinB fin_num_oppeB// addeA subee// add0e.
   by rewrite addeC -sube_eq ?fin_num_adde_defl// subee// => /eqP.
 rewrite -setUitv1// ?bnd_simp; last by rewrite ltr_subl_addr ltr_addl.
-rewrite measureU //; apply/seteqP; split => // x []/=. 
+rewrite measureU //; apply/seteqP; split => // x []/=.
 by rewrite in_itv/= => + xa; rewrite xa ltxx andbF.
 Qed.
 
 Let lebesgue_measure_itvoo (a b : R) :
-  (lebesgue_measure (`]a, b[ : set R) = hlength `]a, b[)%classic.
+  (lebesgue_measure (`]a, b[ : set R) =
+   wlength [the cumulative _ of idfun] `]a, b[)%classic.
 Proof.
 have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt.
 have := lebesgue_measure_itvoc a b.
-rewrite 2!hlength_itv => <-; rewrite -setUitv1// measureU//.
+rewrite 2!wlength_itv => <-; rewrite -setUitv1// measureU//.
 - by have /= -> := lebesgue_measure_set1 b; rewrite adde0.
 - by apply/seteqP; split => // x [/= + xb]; rewrite in_itv/= xb ltxx andbF.
 Qed.
 
 Let lebesgue_measure_itvcc (a b : R) :
-  (lebesgue_measure (`[a, b] : set R) = hlength `[a, b])%classic.
+  (lebesgue_measure (`[a, b] : set R) =
+   wlength [the cumulative _ of idfun] `[a, b])%classic.
 Proof.
 have [ab|ba] := leP a b; last by rewrite set_itv_ge ?measure0// -leNgt.
 have := lebesgue_measure_itvoc a b.
-rewrite 2!hlength_itv => <-; rewrite -setU1itv// measureU//.
+rewrite 2!wlength_itv => <-; rewrite -setU1itv// measureU//.
 - by have /= -> := lebesgue_measure_set1 a; rewrite add0e.
 - by apply/seteqP; split => // x [/= ->]; rewrite in_itv/= ltxx.
 Qed.
 
 Let lebesgue_measure_itvco (a b : R) :
-  (lebesgue_measure (`[a, b[ : set R) = hlength `[a, b[)%classic.
+  (lebesgue_measure (`[a, b[ : set R) =
+   wlength [the cumulative _ of idfun] `[a, b[)%classic.
 Proof.
 have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt.
 have := lebesgue_measure_itvoo a b.
-rewrite 2!hlength_itv => <-; rewrite -setU1itv// measureU//.
+rewrite 2!wlength_itv => <-; rewrite -setU1itv// measureU//.
 - by have /= -> := lebesgue_measure_set1 a; rewrite add0e.
 - by apply/seteqP; split => // x [/= ->]; rewrite in_itv/= ltxx.
 Qed.
 
 Let lebesgue_measure_itv_bnd (x y : bool) (a b : R) :
   lebesgue_measure ([set` Interval (BSide x a) (BSide y b)] : set R) =
-  hlength [set` Interval (BSide x a) (BSide y b)].
+  wlength [the cumulative _ of idfun] [set` Interval (BSide x a) (BSide y b)].
 Proof.
 by move: x y => [|] [|]; [exact: lebesgue_measure_itvco |
   exact: lebesgue_measure_itvcc | exact: lebesgue_measure_itvoo |
@@ -895,7 +823,7 @@ rewrite itv_bnd_infty_bigcup; transitivity (lim (lebesgue_measure \o
   + move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[->/=].
     by move=> /le_trans; apply; rewrite ler_add// ler_nat.
 rewrite (_ : _ \o _ = (fun k => k%:R%:E))//.
-apply/funext => n /=; rewrite lebesgue_measure_itv_bnd hlength_itv/=.
+apply/funext => n /=; rewrite lebesgue_measure_itv_bnd wlength_itv/=.
 rewrite lte_fin;  have [->|n0] := eqVneq n 0%N; first by rewrite addr0 ltxx.
 by rewrite ltr_addl ltr0n lt0n n0 EFinD addeAC EFinN subee ?add0e.
 Qed.
@@ -911,27 +839,33 @@ rewrite itv_infty_bnd_bigcup; transitivity (lim (lebesgue_measure \o
   + move=> m n mn; apply/subsetPset => r/=; rewrite !in_itv/= => /andP[+ ->].
     by rewrite andbT; apply: le_trans; rewrite ler_sub// ler_nat.
 rewrite (_ : _ \o _ = (fun k : nat => k%:R%:E))//.
-apply/funext => n /=; rewrite lebesgue_measure_itv_bnd hlength_itv/= lte_fin.
+apply/funext => n /=; rewrite lebesgue_measure_itv_bnd wlength_itv/= lte_fin.
 have [->|n0] := eqVneq n 0%N; first by rewrite subr0 ltxx.
 rewrite ltr_subl_addr ltr_addl ltr0n lt0n n0 EFinN EFinB fin_num_oppeB// addeA.
 by rewrite subee// add0e.
 Qed.
 
+Let lebesgue_measure_itv_infty_infty :
+  lebesgue_measure ([set` Interval -oo%O +oo%O] : set R) = +oo%E.
+Proof.
+rewrite set_itv_infty_infty -(setUv (`]-oo, 0[)) setCitv.
+rewrite [X in _ `|` (X `|` _) ]set_itvE set0U measureU//; last first.
+  apply/seteqP; split => //= x [] /= /[swap].
+  by rewrite !in_itv/= andbT ltNge => ->//.
+rewrite [X in (X + _)%E]lebesgue_measure_itv_infty_bnd.
+by rewrite [X in (_ + X)%E]lebesgue_measure_itv_bnd_infty.
+Qed.
+
 Lemma lebesgue_measure_itv (i : interval R) :
-  lebesgue_measure ([set` i] : set R) = hlength [set` i].
+  lebesgue_measure ([set` i] : set R) = (if i.1 < i.2 then i.2 - i.1 else 0)%E.
 Proof.
-move: i => [[x a|[|]]] [y b|[|]]; first exact: lebesgue_measure_itv_bnd.
+move: i => [[x a|[|]]] [y b|[|]].
+  by rewrite lebesgue_measure_itv_bnd wlength_itv.
 - by rewrite set_itvE ?measure0.
-- by rewrite lebesgue_measure_itv_bnd_infty hlength_bnd_infty.
-- by rewrite lebesgue_measure_itv_infty_bnd hlength_infty_bnd.
+- by rewrite lebesgue_measure_itv_bnd_infty/= ltry.
+- by rewrite lebesgue_measure_itv_infty_bnd/= ltNyr.
 - by rewrite set_itvE ?measure0.
-- rewrite set_itvE hlength_setT.
-  rewrite (_ : setT = [set` `]-oo, 0[] `|` [set` `[0, +oo[]); last first.
-    by apply/seteqP; split=> // => x _; have [x0|x0] := leP 0 x; [right|left];
-      rewrite /= in_itv//= x0.
-  rewrite measureU//=; try exact: measurable_itv.
-  + by rewrite lebesgue_measure_itv_infty_bnd lebesgue_measure_itv_bnd_infty.
-  + by apply/seteqP; split => // x []/=; rewrite !in_itv/= andbT leNgt => ->.
+- by rewrite lebesgue_measure_itv_infty_infty.
 - by rewrite set_itvE ?measure0.
 - by rewrite set_itvE ?measure0.
 - by rewrite set_itvE ?measure0.
@@ -1893,7 +1827,7 @@ Lemma lebesgue_regularity_outer (D : set R) (eps : R) :
   exists U : set R, [/\ open U , D `<=` U & mu (U `\` D) < eps%:E].
 Proof.
 move=> mD muDpos epspos.
-have /ereal_inf_lt[z [/= M' covDM sMz zDe]] : mu D < mu D + (eps / 2)%:E.
+have /ereal_inf_lt[z [M' covDM sMz zDe]] : mu D < mu D + (eps / 2)%:E.
   by rewrite lte_spaddre ?lte_fin ?divr_gt0// ge0_fin_numE.
 pose e2 n := (eps / 2) / (2 ^ n.+1)%:R.
 have e2pos n : (0 < e2 n)%R by rewrite ?divr_gt0.
@@ -1910,7 +1844,7 @@ have muM n : mu (M n) <= mu (M' n) + (e2 n)%:E.
       by rewrite propeqE; split=> /orP.
     by rewrite !bnd_simp (ltW alb)/= ltr_spaddr.
   rewrite measureU/=.
-  - rewrite !lebesgue_measure_itv !hlength_itv/= !lte_fin alb ltr_spaddr//=.
+  - rewrite !lebesgue_measure_itv/= !lte_fin alb ltr_spaddr//=.
     by rewrite -(EFinD (b + e2 n)) (addrC b) addrK.
   - by apply: sub_sigma_algebra; exact: is_ocitv.
   - by apply: open_measurable; exact: interval_open.
@@ -1936,7 +1870,8 @@ have muU : mu U < mu D + eps%:E.
     by apply: epsilon_trick => //; rewrite divr_ge0// ltW.
   rewrite {2}[eps]splitr EFinD addeA lte_le_add//.
   rewrite (le_lt_trans _ zDe)// -sMz lee_nneseries// => i _.
-  rewrite -hlength_Rhull -lebesgue_measure_itv le_measure//= ?inE.
+  rewrite /= -wlength_Rhull wlength_itv !er_map_idfun.
+  rewrite -lebesgue_measure_itv le_measure//= ?inE.
   - by case: covDM => /(_ i) + _; exact: sub_sigma_algebra.
   - exact: measurable_itv.
   - exact: sub_Rhull.
@@ -2011,7 +1946,7 @@ have mD' : measurable D' by exact: measurableD.
 have [] := lebesgue_regularity_outer mD' _ epspos.
   rewrite (@le_lt_trans _ _ (mu `[a,b]%classic))//.
     by rewrite le_measure ?inE//; exact: subIsetl.
-  by rewrite /= lebesgue_measure_itv /= hlength_itv //= -EFinD -fun_if ltry.
+  by rewrite /= lebesgue_measure_itv //= -EFinD -fun_if ltry.
 move=> U [oU /subsetC + mDeps]; rewrite setCI setCK => nCD'.
 exists (`[a, b] `&` ~` U); split.
 - apply: (subclosed_compact _ (@segment_compact _ a b)) => //.
@@ -2045,7 +1980,10 @@ Lemma lebesgue_regularity_inner_sup (D : set R) (eps : R) : measurable D ->
 Proof.
 move=> mD; have [?|] := ltP (mu D) +oo.
   exact: lebesgue_regularity_innerE_bounded.
-have /sigma_finiteP [/= F RFU [Fsub ffin]] := sigmaT_finite_lebesgue_measure R (*TODO: sigma_finiteT mu should be enough but does not seem to work with holder version of mathcomp/coq *).
+have /sigma_finiteP [F RFU [Fsub ffin]] :=
+  sigmaT_finite_lebesgue_stieltjes_measure [the @cumulative R of idfun]
+  (*TODO: sigma_finiteT mu should be enough but does not seem to work with older
+    versions of MathComp/Coq (Coq <= 8.15?) *).
 rewrite leye_eq => /eqP /[dup] + ->.
 have {1}-> : D = \bigcup_n (F n `&` D) by rewrite -setI_bigcupl -RFU setTI.
 move=> FDp; apply/esym/eq_infty => M.
@@ -2058,7 +1996,7 @@ move/cvgey_ge => /(_ (M + 1)%R) [N _ /(_ _ (lexx N))].
 have [mFN FNoo] := ffin N.
 have [] := @lebesgue_regularity_inner (F N `&` D) _ _ _ ltr01.
 - exact: measurableI.
-- by rewrite (le_lt_trans _ (ffin N).2)// measureIl.
+- 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 => //.
diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v
new file mode 100644
index 000000000..4414860f1
--- /dev/null
+++ b/theories/lebesgue_stieltjes_measure.v
@@ -0,0 +1,520 @@
+(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
+From mathcomp Require Import finmap fingroup perm rat.
+From HB Require Import structures.
+From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
+From mathcomp.classical Require Import functions fsbigop cardinality.
+Require Import reals ereal signed topology numfun normedtype sequences esum.
+Require Import real_interval measure realfun.
+
+(******************************************************************************)
+(*                       Lebesgue Stieltjes Measure                           *)
+(*                                                                            *)
+(* This file contains a formalization of the Lebesgue-Stieltjes measure using *)
+(* the Measure Extension theorem from measure.v.                              *)
+(*                                                                            *)
+(* Reference:                                                                 *)
+(* - Achim Klenke, Probability Theory 2nd edition, 2014                       *)
+(*                                                                            *)
+(*    right_continuous f == the function f is right-continuous                *)
+(*          cumulative R == type of non-decreasing, right-continuous          *)
+(*                          functions (with R : numFieldType)                 *)
+(*                          The HB class is Cumulative.                       *)
+(*                          instance: idfun                                   *)
+(*          ocitv_type R == alias for R : realType                            *)
+(*                 ocitv == set of open-closed intervals ]x, y] where         *)
+(*                          x and y are real numbers                          *)
+(*              R.-ocitv == display for ocitv_type R                          *)
+(*  R.-ocitv.-measurable == semiring of sets of open-closed intervals         *)
+(*           wlength f A := f b - f a with the hull of the set of real        *)
+(*                          numbers A being delimited by a and b              *)
+(* lebesgue_stieltjes_measure f == Lebesgue-Stieltjes measure for f           *)
+(*                          f is a cumulative function.                       *)
+(*                                                                            *)
+(******************************************************************************)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+Import Order.TTheory GRing.Theory Num.Def Num.Theory.
+Import numFieldTopology.Exports.
+
+Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
+
+Reserved Notation "R .-ocitv" (at level 1, format "R .-ocitv").
+Reserved Notation "R .-ocitv.-measurable"
+ (at level 2, format "R .-ocitv.-measurable").
+
+(* TODO: move? *)
+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.
+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} ;
+  cumulative_is_right_continuous : right_continuous f }.
+
+#[short(type=cumulative)]
+HB.structure Definition Cumulative (R : numFieldType) :=
+  { f of isCumulative R f }.
+
+Arguments cumulative_is_nondecreasing {R} _.
+Arguments cumulative_is_right_continuous {R} _.
+
+Lemma nondecreasing_right_continuousP (R : numFieldType) (a : R) (e : R)
+    (f : cumulative R) :
+  e > 0 -> exists d : {posnum R}, f (a + d%:num) <= f a + e.
+Proof.
+move=> e0; move: (cumulative_is_right_continuous f).
+move=> /(_ a)/(@cvgr_dist_lt _ [normedModType R of R^o]).
+move=> /(_ _ e0)[] _ /posnumP[d] => h.
+exists (PosNum [gt0 of (d%:num / 2)]) => //=.
+move: h => /(_ (a + d%:num / 2)) /=.
+rewrite opprD addrA subrr distrC subr0 ger0_norm //.
+rewrite ltr_pdivr_mulr// ltr_pmulr// ltr1n => /(_ erefl).
+rewrite ltr_addl divr_gt0// => /(_ erefl).
+rewrite ler0_norm; last first.
+  by rewrite subr_le0 (cumulative_is_nondecreasing f)// ler_addl.
+by rewrite opprB ltr_subl_addl => fa; exact: ltW.
+Qed.
+
+Section id_is_cumulative.
+Variable R : realType.
+
+Let id_nd : {homo @idfun R : x y / x <= y}.
+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.
+End id_is_cumulative.
+(* /TODO: move? *)
+
+Section itv_semiRingOfSets.
+Variable R : realType.
+Implicit Types (I J K : set R).
+Definition ocitv_type : Type := R.
+
+Definition ocitv := [set `]x.1, x.2]%classic | x in [set: R * R]].
+
+Lemma is_ocitv a b : ocitv `]a, b]%classic.
+Proof. by exists (a, b); split => //=; rewrite in_itv/= andbT. Qed.
+Hint Extern 0 (ocitv _) => solve [apply: is_ocitv] : core.
+
+Lemma ocitv0 : ocitv set0.
+Proof. by exists (1, 0); rewrite //= set_itv_ge ?bnd_simp//= ltr10. Qed.
+Hint Resolve ocitv0 : core.
+
+Lemma ocitvP X : ocitv X <-> X = set0 \/ exists2 x, x.1 < x.2 & X = `]x.1, x.2]%classic.
+Proof.
+split=> [[x _ <-]|[->//|[x xlt ->]]]//.
+case: (boolP (x.1 < x.2)) => x12; first by right; exists x.
+by left; rewrite set_itv_ge.
+Qed.
+
+Lemma ocitvD : semi_setD_closed ocitv.
+Proof.
+move=> _ _ [a _ <-] /ocitvP[|[b ltb]] ->.
+  rewrite setD0; exists [set `]a.1, a.2]%classic].
+  by split=> [//|? ->//||? ? -> ->//]; rewrite bigcup_set1.
+rewrite setDE setCitv/= setIUr -!set_itvI.
+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 /= [].
+  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 /=.
+  move=> /andP[a1x xb1] /andP[b2x xa2].
+  by have := lt_le_trans b2x xb1; case: ltgtP ltb.
+exists ((if a.1 < c then [set `]a.1, c]%classic] else set0) `|`
+        (if d < a.2 then [set `]d, a.2]%classic] else set0)); split.
+- by rewrite finite_setU; do! case: ifP.
+- by move=> ? []; case: ifP => ? // ->//=.
+- by rewrite bigcup_setU; congr (_ `|` _);
+     case: ifPn => ?; rewrite ?bigcup_set1 ?bigcup_set0// set_itv_ge.
+- move=> I J/=; case: ifP => //= ac; case: ifP => //= da [] // -> []// ->.
+    by rewrite inside// => -[].
+  by rewrite setIC inside// => -[].
+Qed.
+
+Lemma ocitvI : setI_closed ocitv.
+Proof.
+move=> _ _ [a _ <-] [b _ <-]; rewrite -set_itvI/=.
+rewrite /Order.meet/= /Order.meet /Order.join/=
+        ?(andbF, orbF)/= ?(meetEtotal, joinEtotal).
+by rewrite -negb_or le_total/=.
+Qed.
+
+Definition ocitv_display : Type -> measure_display. Proof. exact. Qed.
+
+HB.instance Definition _ :=
+  @isSemiRingOfSets.Build (ocitv_display R)
+    ocitv_type (Pointed.class R) ocitv ocitv0 ocitvI ocitvD.
+
+End itv_semiRingOfSets.
+
+Notation "R .-ocitv" := (ocitv_display R) : measure_display_scope.
+Notation "R .-ocitv.-measurable" := (measurable : set (set (ocitv_type R))) :
+  classical_set_scope.
+
+Local Open Scope measure_display_scope.
+
+Section wlength.
+Context {R : realType}.
+Variable (f : R -> R).
+Local Open Scope ereal_scope.
+Implicit Types i j : interval R.
+
+Let g : \bar R -> \bar R := er_map f.
+
+Definition wlength (A : set (ocitv_type R)) : \bar R :=
+  let i := Rhull A in g i.2 - g i.1.
+
+Lemma wlength0 : wlength (set0 : set R) = 0.
+Proof. by rewrite /wlength Rhull0 /= subee. Qed.
+
+Lemma wlength_singleton (r : R) : wlength `[r, r] = 0.
+Proof.
+rewrite /wlength /= asboolT// sup_itvcc//= asboolT//.
+by rewrite asboolT inf_itvcc//= ?subee// inE.
+Qed.
+
+Lemma wlength_setT : wlength setT = +oo%E :> \bar R.
+Proof. by rewrite /wlength RhullT. Qed.
+
+Lemma wlength_itv i : wlength [set` i] = if i.2 > i.1 then g i.2 - g i.1 else 0.
+Proof.
+case: ltP => [/lt_ereal_bnd/neitvP i12|]; first by rewrite /wlength set_itvK.
+rewrite le_eqVlt => /orP[|/lt_ereal_bnd i12]; last first.
+  rewrite -wlength0; congr (wlength _).
+  by apply/eqP/negPn; rewrite -/(neitv _) neitvE -leNgt (ltW i12).
+case: i => -[ba a|[|]] [bb b|[|]] //=.
+- rewrite /= => /eqP[->{b}]; move: ba bb => -[] []; try
+    by rewrite set_itvE wlength0.
+  by rewrite wlength_singleton.
+- by move=> _; rewrite set_itvE wlength0.
+- by move=> _; rewrite set_itvE wlength0.
+Qed.
+
+Lemma wlength_finite_fin_num i : neitv i -> wlength [set` i] < +oo ->
+  ((i.1 : \bar R) \is a fin_num) /\ ((i.2 : \bar R) \is a fin_num).
+Proof.
+move: i => [[ba a|[]] [bb b|[]]] /neitvP //=; do ?by rewrite ?set_itvE ?eqxx.
+by move=> _; rewrite wlength_itv /= ltry.
+by move=> _; rewrite wlength_itv /= ltNye.
+by move=> _; rewrite wlength_itv.
+Qed.
+
+Lemma finite_wlength_itv i : neitv i -> wlength [set` i] < +oo ->
+  wlength [set` i] = (fine (g i.2))%:E - (fine (g i.1))%:E.
+Proof.
+move=> i0 ioo; have [i1f i2f] := wlength_finite_fin_num i0 ioo.
+rewrite fineK; last first.
+  by rewrite /g; move: i2f; case: (ereal_of_itv_bound i.2).
+rewrite fineK; last first.
+  by rewrite /g; move: i1f; case: (ereal_of_itv_bound i.1).
+rewrite wlength_itv; case: ifPn => //; rewrite -leNgt le_eqVlt => /predU1P[->|].
+  by rewrite subee// /g; move: i1f; case: (ereal_of_itv_bound i.1).
+by move/lt_ereal_bnd/ltW; rewrite leNgt; move: i0 => /neitvP => ->.
+Qed.
+
+Lemma wlength_itv_bnd (a b : R) (x y : bool) : (a <= b)%R ->
+  wlength [set` Interval (BSide x a) (BSide y b)] = (f b - f a)%:E.
+Proof.
+move=> ab; rewrite wlength_itv/= lte_fin lt_neqAle ab andbT.
+by have [-> /=|/= ab'] := eqVneq a b; rewrite ?subrr// EFinN EFinB.
+Qed.
+
+Lemma wlength_infty_bnd b r :
+  wlength [set` Interval -oo%O (BSide b r)] = +oo :> \bar R.
+Proof. by rewrite wlength_itv /= ltNye. Qed.
+
+Lemma wlength_bnd_infty b r :
+  wlength [set` Interval (BSide b r) +oo%O] = +oo :> \bar R.
+Proof. by rewrite wlength_itv /= ltey. Qed.
+
+Lemma pinfty_wlength_itv i : wlength [set` i] = +oo ->
+  (exists s r, i = Interval -oo%O (BSide s r) \/ i = Interval (BSide s r) +oo%O)
+  \/ i = `]-oo, +oo[.
+Proof.
+rewrite wlength_itv; case: i => -[ba a|[]] [bb b|[]] //= => [|_|_|].
+- by case: ifPn.
+- by left; exists ba, a; right.
+- by left; exists bb, b; left.
+- by right.
+Qed.
+
+Lemma wlength_itv_ge0 (ndf : {homo f : x y / (x <= y)%R}) i :
+  0 <= wlength [set` i].
+Proof.
+rewrite wlength_itv; case: ifPn => //; case: (i.1 : \bar _) => [r| |].
+- by rewrite suber_ge0// => /ltW /(le_er_map ndf).
+- by rewrite ltNge leey.
+- by case: (i.2 : \bar _) => //= [r _]; rewrite leey.
+Qed.
+
+Lemma wlength_Rhull (A : set R) : wlength [set` Rhull A] = wlength A.
+Proof. by rewrite /wlength Rhull_involutive. Qed.
+
+Lemma le_wlength_itv (ndf : {homo f : x y / (x <= y)%R}) i j :
+  {subset i <= j} -> wlength [set` i] <= wlength [set` j].
+Proof.
+set I := [set` i]; set J := [set` j].
+have [->|/set0P I0] := eqVneq I set0; first by rewrite wlength0 wlength_itv_ge0.
+have [J0|/set0P J0] := eqVneq J set0.
+  by move/subset_itvP; rewrite -/J J0 subset0 -/I => ->.
+move=> /subset_itvP ij; apply: lee_sub => /=.
+  have [ui|ui] := asboolP (has_ubound I).
+    have [uj /=|uj] := asboolP (has_ubound J); last by rewrite leey.
+    rewrite lee_fin; apply: ndf; apply/le_sup => //.
+    by move=> r Ir; exists r; split => //; apply: ij.
+  have [uj /=|//] := asboolP (has_ubound J).
+  by move: ui; have := subset_has_ubound ij uj.
+have [lj /=|lj] := asboolP (has_lbound J); last by rewrite leNye.
+have [li /=|li] := asboolP (has_lbound I); last first.
+  by move: li; have := subset_has_lbound ij lj.
+rewrite lee_fin; apply/ndf/le_inf => //.
+move=> r [r' Ir' <-{r}]; exists (- r')%R.
+by split => //; exists r' => //; apply: ij.
+Qed.
+
+Lemma le_wlength (ndf : {homo f : x y / (x <= y)%R}) :
+  {homo wlength : A B / A `<=` B >-> A <= B}.
+Proof.
+move=> a b /le_Rhull /(le_wlength_itv ndf).
+by rewrite (wlength_Rhull a) (wlength_Rhull b).
+Qed.
+
+End wlength.
+
+Section wlength_extension.
+Context {R : realType}.
+
+Lemma wlength_semi_additive (f : R -> R) : semi_additive (wlength f).
+Proof.
+move=> /= I n /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym-/funext {I}->.
+move=> Itriv [[/= a1 a2] _] /esym /[dup] + ->.
+rewrite wlength_itv ?lte_fin/= -EFinB.
+case: ifPn => a12; last first.
+  pose I i := `](b i).1, (b i).2]%classic.
+  rewrite set_itv_ge//= -(bigcup_mkord _ I) /I => /bigcup0P I0.
+  by under eq_bigr => i _ do rewrite I0//= wlength0; rewrite big1.
+set A := `]a1, a2]%classic.
+rewrite -bigcup_pred; set P := xpredT; rewrite (eq_bigl P)//.
+move: P => P; have [p] := ubnP #|P|; elim: p => // p IHp in P a2 a12 A *.
+rewrite ltnS => cP /esym AE.
+have : A a2 by rewrite /A /= in_itv/= lexx andbT.
+rewrite AE/= => -[i /= Pi] a2bi.
+case: (boolP ((b i).1 < (b i).2)) => bi; last by rewrite itv_ge in a2bi.
+have {}a2bi : a2 = (b i).2.
+  apply/eqP; rewrite eq_le (itvP a2bi)/=.
+  suff: A (b i).2 by move=> /itvP->.
+  by rewrite AE; exists i=> //=; rewrite in_itv/= lexx andbT.
+rewrite {a2}a2bi in a12 A AE *.
+rewrite (bigD1 i)//= wlength_itv ?lte_fin/= bi !EFinD -addeA.
+congr (_ + _)%E; apply/eqP; rewrite addeC -sube_eq// 1?adde_defC//.
+rewrite ?EFinN oppeK addeC; apply/eqP.
+have [a1bi|a1bi] := eqVneq a1 (b i).1.
+  rewrite {a1}a1bi in a12 A AE {IHp} *; rewrite subee ?big1// => j.
+  move=> /andP[Pj Nji]; rewrite wlength_itv ?lte_fin/=; case: ifPn => bj//.
+  exfalso; have /trivIsetP/(_ j i I I Nji) := Itriv.
+  pose m := ((b j).1 + (b j).2) / 2%:R.
+  have mbj : `](b j).1, (b j).2]%classic m.
+     by rewrite /= !in_itv/= ?(midf_lt, midf_le)//= ltW.
+  rewrite -subset0 => /(_ m); apply; split=> //.
+  by suff: A m by []; rewrite AE; exists j.
+have a1b2 j : P j -> (b j).1 < (b j).2 -> a1 <= (b j).2.
+  move=> Pj bj; suff /itvP-> : A (b j).2 by [].
+  by rewrite AE; exists j => //=; rewrite ?in_itv/= bj/=.
+have a1b j : P j -> (b j).1 < (b j).2 -> a1 <= (b j).1.
+  move=> Pj bj; case: ltP=> // bj1a.
+  suff : A a1 by rewrite /A/= in_itv/= ltxx.
+  by rewrite AE; exists j; rewrite //= in_itv/= bj1a//= a1b2.
+have bbi2 j : P j -> (b j).1 < (b j).2 -> (b j).2 <= (b i).2.
+  move=> Pj bj; suff /itvP-> : A (b j).2 by [].
+  by rewrite AE; exists j => //=; rewrite ?in_itv/= bj/=.
+apply/IHp.
+- by rewrite lt_neqAle a1bi/= a1b.
+- rewrite (leq_trans _ cP)// -(cardID (pred1 i) P).
+  rewrite [X in (_ < X + _)%N](@eq_card _ _ (pred1 i)); last first.
+    by move=> j; rewrite !inE andbC; case: eqVneq => // ->.
+  rewrite ?card1 ?ltnS// subset_leq_card//.
+  by apply/fintype.subsetP => j; rewrite -topredE/= !inE andbC.
+apply/seteqP; split=> /= [x [j/= /andP[Pj Nji]]|x/= xabi].
+  case: (boolP ((b j).1 < (b j).2)) => bj; last by rewrite itv_ge.
+  apply: subitvP; rewrite subitvE ?bnd_simp a1b//= leNgt.
+  have /trivIsetP/(_ j i I I Nji) := Itriv.
+  rewrite -subset0 => /(_ (b j).2); apply: contra_notN => /= bi1j2.
+  by rewrite !in_itv/= bj !lexx bi1j2 bbi2.
+have: A x.
+  rewrite /A/= in_itv/= (itvP xabi)/= ltW//.
+  by rewrite (le_lt_trans _ bi) ?(itvP xabi).
+rewrite AE => -[j /= Pj xbj].
+exists j => //=.
+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)) :
+  (0 <= wlength f I)%E.
+Proof.
+by rewrite -(wlength0 f) le_wlength//; exact: cumulative_is_nondecreasing.
+Qed.
+
+#[local] Hint Extern 0 (0%:E <= wlength _ _) => solve[apply: wlength_ge0] : core.
+
+HB.instance Definition _ (f : cumulative 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
+    (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)).
+Proof.
+move=> Dab h; have [ab|ab] := leP a0 b0; last first.
+  apply (@le_trans _ _ 0).
+    by rewrite subr_le0 cumulative_is_nondecreasing// ltW.
+  rewrite big_seq sumr_ge0// => i iD.
+  by rewrite subr_ge0 cumulative_is_nondecreasing// Dab.
+have mab k : [set` D] k -> R.-ocitv.-measurable `]a k, b k]%classic by [].
+move: h; rewrite -bigcup_fset.
+move/(@content_sub_fsum _ R _ [the content _ _ of wlength f] _ [set` D]
+    `]a0, b0]%classic (fun x => `](a x), (b x)]%classic) (finite_fset D) mab
+  (is_ocitv _ _)) => /=.
+rewrite wlength_itv_bnd// -lee_fin => /le_trans; apply.
+rewrite -sumEFin fsbig_finite//= set_fsetK// big_seq [in X in (_ <= X)%E]big_seq.
+by apply: lee_sum => i iD; rewrite wlength_itv_bnd// Dab.
+Qed.
+
+Lemma wlength_sigma_sub_additive (f : cumulative R) :
+  sigma_sub_additive (wlength f).
+Proof.
+move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE.
+move=> [a _ <-]; rewrite wlength_itv ?lte_fin/= -EFinB => lebig.
+case: ifPn => a12; last by rewrite nneseries_esum ?esum_ge0.
+wlog wlogh : b A AE lebig / forall n, (b n).1 <= (b n).2.
+  move=> /= h.
+  set A' := fun n => if (b n).1 >= (b n).2 then set0 else A n.
+  set b' := fun n => if (b n).1 >= (b n).2 then (0, 0) else b n.
+  rewrite [X in (_ <= X)%E](_ : _ = \sum_(n <oo) wlength f (A' n))%E; last first.
+    apply: (@eq_eseriesr _ (wlength f \o A) (wlength f \o A')) => k.
+    rewrite /= /A' AE; case: ifPn => // bn.
+    by rewrite set_itv_ge//= bnd_simp -leNgt.
+  apply: (h b').
+  - move=> k; rewrite /A'; case: ifPn => // bk.
+    by rewrite set_itv_ge//= bnd_simp -leNgt /b' bk.
+  - by rewrite AE /b' (negbTE bk).
+  - apply: (subset_trans lebig); apply subset_bigcup => k _.
+    rewrite /A' AE; case: ifPn => bk //.
+    by rewrite subset0 set_itv_ge//= bnd_simp -leNgt.
+  - by move=> k; rewrite /b'; case: ifPn => //; rewrite -ltNge => /ltW.
+apply/lee_addgt0Pr => _/posnumP[e].
+rewrite [e%:num]splitr [in leRHS]EFinD addeA -lee_subl_addr//.
+apply: le_trans (epsilon_trick _ _ _) => //=.
+have [c ce] := nondecreasing_right_continuousP a.1 f [gt0 of e%:num / 2].
+have [D De] : exists D : nat -> {posnum R}, forall i,
+    f ((b i).2 + (D i)%:num) <= f ((b i).2) + (e%:num / 2) / 2 ^ i.+1.
+  suff : forall i, exists di : {posnum R},
+      f ((b i).2 + di%:num) <= f ((b i).2) + (e%:num / 2) / 2 ^ i.+1.
+    by move/choice => -[g hg]; exists g.
+  move=> k; apply nondecreasing_right_continuousP => //.
+  by rewrite divr_gt0 // exprn_gt0.
+have acbd : `[ a.1 + c%:num / 2, a.2] `<=`
+            \bigcup_i `](b i).1, (b i).2 + (D i)%:num[%classic.
+  apply: (@subset_trans _ `]a.1, a.2]).
+    move=> r; rewrite /= !in_itv/= => /andP [+ ->].
+    by rewrite andbT; apply: lt_le_trans; rewrite ltr_addl.
+  apply: (subset_trans lebig) => r [n _ Anr]; exists n => //.
+  move: Anr; rewrite AE /= !in_itv/= => /andP [->]/= /le_lt_trans.
+  by apply; rewrite ltr_addl.
+have := @segment_compact _ (a.1 + c%:num / 2) a.2; rewrite compact_cover.
+have obd k : [set: nat] k -> open `](b k).1, ((b k).2 + (D k)%:num)[%classic.
+  by move=> _; exact: interval_open.
+move=> /(_ _ _ _ obd acbd){obd acbd}.
+case=> X _ acXbd.
+rewrite /cover in acXbd.
+rewrite -EFinD.
+apply: (@le_trans _ _ (\sum_(i <- X) (wlength f `](b i).1, (b i).2]%classic) +
+    \sum_(i <- X) (f ((b i).2 + (D i)%:num)%R - f (b i).2)%:E)%E).
+  apply: (@le_trans _ _ (f a.2 - f (a.1 + c%:num / 2))%:E).
+    rewrite lee_fin -addrA -opprD ler_sub// (le_trans _ ce)//.
+    rewrite cumulative_is_nondecreasing//.
+    by rewrite ler_add2l ler_pdivr_mulr// ler_pmulr// ler1n.
+  apply: (@le_trans _ _
+      (\sum_(i <- X) (f ((b i).2 + (D i)%:num) - f (b i).1)%:E)%E).
+    rewrite sumEFin lee_fin cumulative_content_sub_fsum//.
+      by move=> k kX; rewrite (@le_trans _ _ (b k).2)// ler_addl.
+    apply: subset_trans.
+      exact/(subset_trans _ acXbd)/subset_itv_oc_cc.
+    move=> x [k kX] kx; rewrite -bigcup_fset; exists k => //.
+    by move: x kx; exact: subset_itv_oo_oc.
+  rewrite addeC -big_split/=; apply: lee_sum => k _.
+  by rewrite !(EFinB, wlength_itv_bnd)// addeA subeK.
+rewrite -big_split/= nneseries_esum//; last by move=> k _; rewrite adde_ge0.
+rewrite esum_ge//; exists [set` X] => //; rewrite fsbig_finite//= set_fsetK.
+rewrite big_seq [in X in (_ <= X)%E]big_seq; apply: lee_sum => k kX.
+by rewrite AE lee_add2l// lee_fin ler_subl_addl natrX De.
+Qed.
+
+HB.instance Definition _ (f : cumulative R) :=
+  Content_SubSigmaAdditive_isMeasure.Build _ _ _
+    (wlength f) (wlength_sigma_sub_additive f).
+
+Lemma wlength_sigma_finite (f : R -> R) :
+  sigma_finite [set: (ocitv_type R)] (wlength f).
+Proof.
+exists (fun k => `](- k%:R), k%:R]%classic).
+  apply/esym; rewrite -subTset => /= x _ /=.
+  exists `|(floor `|x|%R + 1)%R|%N; rewrite //= in_itv/=.
+  rewrite !natr_absz intr_norm intrD -RfloorE.
+  suff: `|x| < `|Rfloor `|x| + 1| by rewrite ltr_norml => /andP[-> /ltW->].
+  rewrite [ltRHS]ger0_norm//.
+    by rewrite (le_lt_trans _ (lt_succ_Rfloor _))// ?ler_norm.
+  by rewrite addr_ge0// -Rfloor0 le_Rfloor.
+move=> k; split => //; rewrite wlength_itv /= -EFinB.
+by case: ifP; rewrite ltey.
+Qed.
+
+Definition lebesgue_stieltjes_measure (f : cumulative R) :=
+  measure_extension [the measure _ _ of wlength f].
+HB.instance Definition _ (f : cumulative R) :=
+  Measure.on (lebesgue_stieltjes_measure f).
+
+(* TODO: this ought to be turned into a Let but older version of mathcomp/coq
+   does not seem to allow, try to change asap *)
+Lemma sigmaT_finite_lebesgue_stieltjes_measure (f : cumulative R) :
+  sigma_finite setT (lebesgue_stieltjes_measure f).
+Proof. exact/measure_extension_sigma_finite/wlength_sigma_finite. Qed.
+
+HB.instance Definition _ (f : cumulative R) := @isSigmaFinite.Build _ _ _
+  (lebesgue_stieltjes_measure f) (sigmaT_finite_lebesgue_stieltjes_measure f).
+
+End wlength_extension.
+Arguments lebesgue_stieltjes_measure {R}.
+
+Section lebesgue_stieltjes_measure.
+Variable R : realType.
+Let gitvs := [the measurableType _ of salgebraType (@ocitv R)].
+
+Lemma lebesgue_stieltjes_measure_unique (f : cumulative 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.
+Proof.
+move=> muE X mX; apply: measure_extension_unique => //=.
+  exact: wlength_sigma_finite.
+by move=> A mA; rewrite -muE// -measurable_mu_extE.
+Qed.
+
+End lebesgue_stieltjes_measure.
diff --git a/theories/probability.v b/theories/probability.v
index aa7ca3d16..6e59aad18 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -4,6 +4,7 @@ From mathcomp Require Import ssralg poly ssrnum ssrint interval finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality.
 From HB Require Import structures.
+Require Import exp numfun lebesgue_measure lebesgue_integral.
 Require Import reals ereal signed topology normedtype sequences esum measure.
 Require Import exp numfun lebesgue_measure lebesgue_integral.
 
diff --git a/theories/reals.v b/theories/reals.v
index b401650ba..b0fb59543 100644
--- a/theories/reals.v
+++ b/theories/reals.v
@@ -770,53 +770,59 @@ End CeilTheory.
 (* -------------------------------------------------------------------- *)
 Section Sup.
 Context {R : realType}.
+Implicit Types A B : set R.
 
-Lemma le_down (S : set R) : S `<=` down S.
-Proof. by move=> x xS; apply/downP; exists x. Qed.
+Lemma le_down A : A `<=` down A.
+Proof. by move=> x xA; apply/downP; exists x. Qed.
 
-Lemma downK (S : set R) : down (down S) = down S.
+Lemma downK A : down (down A) = down A.
 Proof.
-rewrite predeqE => x; split.
-- case/downP => y /downP[z Sz yz xy].
-  by apply/downP; exists z => //; rewrite (le_trans xy).
-- by move=> Sx; apply/downP; exists x.
+rewrite predeqE => x; split; last by move=> Ax; apply/downP; exists x.
+case/downP => y /downP[z Az yz xy].
+by apply/downP; exists z => //; rewrite (le_trans xy).
 Qed.
 
-Lemma has_sup_down (S : set R) : has_sup (down S) <-> has_sup S.
+Lemma has_sup_down A : has_sup (down A) <-> has_sup A.
 Proof.
-split=> -[nzS nzubS].
-  case: nzS=> x /downP[y yS le_xy]; split; first by exists y.
-  case: nzubS=> u /ubP ubS; exists u; apply/ubP=> z zS.
-  by apply/ubS; apply/downP; exists z.
-case: nzS=> x xS; split; first by exists x; apply/le_down.
-case: nzubS=> u /ubP ubS; exists u; apply/ubP=> y /downP [].
-by move=> z zS /le_trans; apply; apply/ubS.
+split=> -[nzA nzubA].
+  case: nzA => x /downP[y yS le_xy]; split; first by exists y.
+  case: nzubA=> u /ubP ubA; exists u; apply/ubP=> z zS.
+  by apply/ubA; apply/downP; exists z.
+case: nzA => x xA; split; first by exists x; apply/le_down.
+case: nzubA => u /ubP ubA; exists u; apply/ubP=> y /downP [].
+by move=> z zA /le_trans; apply; apply/ubA.
 Qed.
 
-Lemma le_sup (S1 S2 : set R) :
-  S1 `<=` down S2 -> nonempty S1 -> has_sup S2
-    -> sup S1 <= sup S2.
+Lemma le_sup A B : A `<=` down B -> nonempty A -> has_sup B ->
+  sup A <= sup B.
 Proof.
-move=> le_S12 nz_S1 hs_S2; have hs_S1: has_sup S1.
-  split=> //; case: hs_S2=> _ [x ubx].
-  exists x; apply/ubP=> y /le_S12 /downP[z zS2 le_yz].
+move=> le_AB nz_A hs_B; have hs_A: has_sup A.
+  split=> //; case: hs_B => _ [x ubx].
+  exists x; apply/ubP=> y /le_AB /downP[z zB le_yz].
   by apply/(le_trans le_yz); move/ubP: ubx; apply.
 rewrite leNgt -subr_gt0; apply/negP => lt_sup.
-case: (sup_adherent lt_sup hs_S1 )=> x /le_S12 xdS2.
-rewrite subKr => lt_S2x; case/downP: xdS2=> z zS2.
-move/(lt_le_trans lt_S2x); rewrite ltNge.
-by move/ubP: (sup_upper_bound hs_S2) => ->.
+case: (sup_adherent lt_sup hs_A )=> x /le_AB xdB.
+rewrite subKr => lt_Bx; case/downP: xdB => z zB.
+move/(lt_le_trans lt_Bx); rewrite ltNge.
+by move/ubP : (sup_upper_bound hs_B) => ->.
 Qed.
 
-Lemma sup_down (S : set R) : sup (down S) = sup S.
+Lemma le_inf A B : -%R @` B `<=` down (-%R @` A) -> nonempty B -> has_inf A ->
+  inf A <= inf B.
 Proof.
-have [supS|supNS] := pselect (has_sup S); last first.
+move=> SBA AB Ai; rewrite ler_oppl opprK le_sup// ?has_inf_supN//.
+exact/nonemptyN.
+Qed.
+
+Lemma sup_down A : sup (down A) = sup A.
+Proof.
+have [supA|supNA] := pselect (has_sup A); last first.
   by rewrite !sup_out // => /has_sup_down.
-have supDS : has_sup (down S) by apply/has_sup_down.
+have supDA : has_sup (down A) by apply/has_sup_down.
 apply/eqP; rewrite eq_le !le_sup //.
-  by case: supS => -[x xS] _; exists x; apply/le_down.
-  rewrite downK; exact: le_down.
-  by case: supS.
+- by case: supA => -[x xA] _; exists x; apply/le_down.
+- by rewrite downK; exact: le_down.
+- by case: supA.
 Qed.
 
 Lemma lt_sup_imfset {T : Type} (F : T -> R) l :
@@ -835,8 +841,8 @@ Lemma lt_inf_imfset {T : Type} (F : T -> R) l :
   exists2 x, F x < l & inf [set y | exists x, y = F x] <= F x.
 Proof.
 set P := [set y | _]; move=> hs; rewrite -subr_gt0.
-move=> /inf_adherent/(_ hs)[_ [x ->]]; rewrite addrA [_ + l]addrC addrK.
-by move=> ltFxl; exists x=> //; move/lbP : (inf_lower_bound hs) => -> //; exists x.
+move=> /inf_adherent/(_ hs)[_ [x ->]]; rewrite addrCA subrr addr0 => ltFxl.
+by exists x=> //; move/lbP : (inf_lower_bound hs) => -> //; exists x.
 Qed.
 
 End Sup.