proposition: Lemma integralZl_indic (f : R -> set T) (k : R) : ((k < 0)%R -> f k = set0) -> measurable (f k) -> \int[m]_(x in D) (k * \1_(f k) x)%:E = k%:E * \int[m]_(x in D) (\1_(f k) x)%:E.
proof: Proof. move=> fk0 mfk; have [k0|k0] := ltP k 0%R. rewrite integral0_eq//; last by move=> x _; rewrite fk0// indic0 mulr0. by rewrite integral0_eq ?mule0// => x _; rewrite fk0// indic0. under eq_integral do rewrite EFinM. rewrite ge0_integralZl//; first exact/EFin_measurable_fun. by move=> y _; rewrite lee_fin. 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