proposition: Lemma emeasurable_funB D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \- g).
proof: Proof. by move=> mf mg mD; apply: emeasurable_funD => //; exact: measurableT_comp. 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