proposition: Lemma integrableN f : mu_int f -> mu_int (-%E \o f).
proof: Proof. move=> /integrableP[mf foo]; apply/integrableP; split; last first. by rewrite /comp; under eq_fun do rewrite abseN. by rewrite /comp; apply: measurableT_comp =>//; exact: measurable_oppe. 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