proposition: Lemma sintegral_EFin_cst (x : {nonneg R}) : sintegral mu (cst x%:num \_ D) = x%:num%:E * mu D.
proof: Proof. rewrite sintegralE (fsbig_widen _ [set 0%R; x%:num])/=. - have [->|x0] := eqVneq x%:num 0%R; first by rewrite setUid fsbig_set1 !mul0e. rewrite fsbigU0//=; last by move=> y [->]/esym; apply/eqP. rewrite !fsbig_set1 mul0e add0e preimage_restrict//. by rewrite ifN ?set0U ?setIidl//= notin_set => /esym; exact/eqP. - by move=> y [t _ <-] /=; rewrite /patch; case: ifPn; [right|left]. - by move=> y [_ /=/preimage10->]; rewrite measure0 mule0. 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