diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 096254f1dd..89e41d56b6 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -31,6 +31,9 @@
     `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned
 	into local `Let`'s
 
+- in `lebesgue_integral.v`:
+  + lemma `cst_mfun_subproof` now a `Let`
+
 ### Renamed
 
 - in `constructive_ereal.v`:
@@ -55,15 +58,23 @@
 ### Generalized
 
 - in `lebesgue_integral.v`:
-  + generalized from `realType` to `sigmaRingType`
+  + generalized from `sigmaRingType`/`realType` to `sigmaRingType`
     * mixin `isMeasurableFun`
     * structure `MeasurableFun`
 	* definition `mfun`
+    * lemmas `mfun_rect`, `mfun_valP`, `mfuneqP`
+  + generalized from `measurableType`/`realType` to `sigmaRingType`/`realType`
+    * lemmas `cst_mfun_subproof`, `mfun_cst`
+    * definition `cst_mfun`
 
 ### Deprecated
 
 ### Removed
 
+- in `lebesgue_integral.v`:
+  + definition `cst_mfun`
+  + lemma `mfun_cst`
+
 ### Infrastructure
 
 ### Misc
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 7807da6f3b..5667b439ae 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -257,8 +257,8 @@ Definition mfun_key : pred_key mfun. Proof. exact. Qed.
 Canonical mfun_keyed := KeyedPred mfun_key.
 End mfun_pred.
 
-Section mfun_realType.
-Context {d} {aT : sigmaRingType d} {rT : realType}.
+Section mfun.
+Context {d d'} {aT : sigmaRingType d} {rT : sigmaRingType d'}.
 Notation T := {mfun aT >-> rT}.
 Notation mfun := (@mfun _ _ aT rT).
 
@@ -286,17 +286,15 @@ Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed.
 
 HB.instance Definition _ := [Choice of {mfun aT >-> rT} by <:].
 
-Lemma cst_mfun_subproof x : @isMeasurableFun d _ aT rT (cst x).
-Proof. by split. Qed.
-HB.instance Definition _ x := @cst_mfun_subproof x.
-Definition cst_mfun x := [the {mfun aT >-> rT} of cst x].
+End mfun.
 
-Lemma mfun_cst x : @cst_mfun x =1 cst x. Proof. by []. Qed.
+Section mfun_realType.
+Context {d} {aT : sigmaRingType d} {rT : realType}.
 
-End mfun_realType.
+Let cst_mfun_subproof x : @isMeasurableFun d _ aT rT (cst x).
+Proof. by split. Qed.
 
-Section mfun.
-Context {d} {aT : measurableType d} {rT : realType}.
+HB.instance Definition _ x := @cst_mfun_subproof x.
 
 HB.instance Definition _ := @isMeasurableFun.Build _ _ _ rT
   (@normr rT rT) (@measurable_normr rT setT).
@@ -304,6 +302,11 @@ HB.instance Definition _ := @isMeasurableFun.Build _ _ _ rT
 HB.instance Definition _ :=
   isMeasurableFun.Build _ _ _ _ (@expR rT) (@measurable_expR rT).
 
+End mfun_realType.
+
+Section mfun_measurableType.
+Context {d d'} {aT : measurableType d} {rT : measurableType d'}.
+
 Lemma measurableT_comp_subproof (f : {mfun _ >-> rT}) (g : {mfun aT >-> rT}) :
   measurable_fun setT (f \o g).
 Proof. exact: measurableT_comp. Qed.
@@ -311,7 +314,7 @@ Proof. exact: measurableT_comp. Qed.
 HB.instance Definition _ (f : {mfun _ >-> rT}) (g : {mfun aT >-> rT}) :=
   isMeasurableFun.Build _ _ _ _ (f \o g) (measurableT_comp_subproof _ _).
 
-End mfun.
+End mfun_measurableType.
 
 Section ring.
 Context d (aT : measurableType d) (rT : realType).
@@ -370,7 +373,7 @@ HB.instance Definition _ D mD := @indic_mfun_subproof D mD.
 Definition indic_mfun (D : set aT) (mD : measurable D) :=
   [the {mfun aT >-> rT} of mindic mD].
 
-HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst_mfun k).
+HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst k).
 Definition scale_mfun k f := [the {mfun aT >-> rT} of k \o* f].
 
 Lemma max_mfun_subproof f g : @isMeasurableFun d _ aT rT (f \max g).