proposition: Lemma integralZl r : \int[mu]_(x in D) (r%:E * f x) = r%:E * \int[mu]_(x in D) f x.
proof: Proof. have [r0|r0|->] := ltgtP r 0%R; last first. by under eq_fun do rewrite mul0e; rewrite mul0e integral0. - rewrite [in LHS]integralE// gt0_funeposM// gt0_funenegM//. rewrite (ge0_integralZl_EFin _ _ _ _ (ltW r0)) //; last first. exact: measurable_funepos. rewrite (ge0_integralZl_EFin _ _ _ _ (ltW r0)) //; last first. exact: measurable_funeneg. rewrite -muleBr 1?[in RHS]integralE//. exact: integrable_add_def. - rewrite [in LHS]integralE// lt0_funeposM// lt0_funenegM//. rewrite ge0_integralZl_EFin //; last 2 first. + exact: measurable_funeneg. + by rewrite -lerNr oppr0 ltW. rewrite ge0_integralZl_EFin //; last 2 first. + exact: measurable_funepos. + by rewrite -lerNr oppr0 ltW. rewrite -mulNe -EFinN opprK addeC EFinN mulNe -muleBr //; last first. exact: integrable_add_def. by rewrite [in RHS]integralE. 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