fix for compatibility with earlier versions

Author: affeldt-aist

theories/lebesgue_measure.v

@@ -387,7 +387,9 @@ Qed.
 Definition lebesgue_measure := measure_extension [the measure _ _ of hlength].
 HB.instance Definition _ := Measure.on lebesgue_measure.
 
-Let sigmaT_finite_lebesgue_measure : sigma_finite setT 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.
 Proof. exact/measure_extension_sigma_finite/hlength_sigma_finite. Qed.
 
 HB.instance Definition _ := @isSigmaFinite.Build _ _ _
@@ -2031,7 +2033,7 @@ 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]] := sigma_finiteT mu.
+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 *).
 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.