proposition: Lemma integral_cst d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) (D : set T) : d.-measurable D -> forall r, \int[mu]_(x in D) (cst r) x = r * mu D.
proof: Proof. move=> mD; have [D0 r|D0 [r| |]] := eqVneq (mu D) 0. by rewrite (ae_eq_integral (cst 0))// ?integral0 ?D0 ?mule0//; exact: ae_eq0. - by rewrite integral_cstr. - by rewrite integral_csty// gt0_mulye// lt0e D0/=. - by rewrite integral_cstNy// gt0_mulNye// lt0e D0/=. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun