better behaved Rintegral_cst (#1833)

* better behaved Rintegral_cst

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -13,6 +13,9 @@
 - in set_interval.v
   + `itv_is_open_unbounded`, `itv_is_oo`, `itv_open_ends` (Prop to bool)
 
+- in `lebesgue_Rintegrable.v`:
+  + lemma `Rintegral_cst` (does not use `cst` anymore)
+
 ### Renamed
 - in set_interval.v
   + `itv_is_ray` -> `itv_is_open_unbounded`

theories/lebesgue_integral_theory/lebesgue_Rintegral.v

@@ -146,7 +146,7 @@ Lemma Rintegral_set0 f : \int[mu]_(x in set0) f x = 0.
 Proof. by rewrite /Rintegral integral_set0. Qed.
 
 Lemma Rintegral_cst D : d.-measurable D ->
-  forall r, \int[mu]_(x in D) (cst r) x = r * fine (mu D).
+  forall r, \int[mu]_(_ in D) r = r * fine (mu D).
 Proof.
 move=> mD r; rewrite /Rintegral/= integral_cst//.
 have := leey (mu D); rewrite le_eqVlt => /predU1P[->/=|muy]; last first.