proposition: Lemma integrable_add_def f : mu_int f -> \int[mu]_(x in D) f^\+ x +? - \int[mu]_(x in D) f^\- x.
proof: Proof. move=> /integrableP[mf]; rewrite -[fun x => _]/(abse \o f) fune_abse => foo. rewrite ge0_integralD // in foo; last 2 first. - exact: measurable_funepos. - exact: measurable_funeneg. apply: ltpinfty_adde_def. - by apply: le_lt_trans foo; rewrite leeDl// integral_ge0. - by rewrite inE (@le_lt_trans _ _ 0)// leeNl oppe0 integral_ge0. 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