diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 9f6f518d75..7c7f88912c 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -3391,8 +3391,8 @@ have [r0|r0|->] := ltgtP r 0%R.
 Qed.
 
 Lemma integralZr r :
-  \int[mu]_(x in D) (f x * r%:E) = r%:E * \int[mu]_(x in D) f x.
-Proof. by rewrite -integralZl; under eq_integral do rewrite muleC. Qed.
+  \int[mu]_(x in D) (f x * r%:E) = (\int[mu]_(x in D) f x) * r%:E.
+Proof. by rewrite muleC -integralZl; under eq_integral do rewrite muleC. Qed.
 
 End linearityZ.
 #[deprecated(since="mathcomp-analysis 0.6.4", note="use `integralZl` instead")]
diff --git a/theories/probability.v b/theories/probability.v
index 37aed52156..3a6c382614 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -159,7 +159,7 @@ Qed.
 
 Lemma expectationM (X : {RV P >-> R}) (iX : P.-integrable [set: T] (EFin \o X))
   (k : R) : 'E_P[k \o* X] = k%:E * 'E_P [X].
-Proof. by rewrite unlock -integralZr. Qed.
+Proof. by rewrite unlock muleC -integralZr. Qed.
 
 Lemma expectation_ge0 (X : {RV P >-> R}) :
   (forall x, 0 <= X x)%R -> 0 <= 'E_P[X].