proposition: Lemma integral_funeneg_lt_pinfty f : mu_int f -> \int[mu]_(x in D) f^\- x < +oo.
proof: Proof. move=> /integrableP[mf]; apply: le_lt_trans; apply: ge0_le_integral => //. - exact: measurable_funeneg. - exact: measurableT_comp. - move=> x Dx; have [fx0|/ltW fx0] := leP (f x) 0. rewrite lee0_abs// /funeneg. by move: fx0; rewrite -{1}oppe0 -leeNr => /max_idPl ->. rewrite gee0_abs// /funeneg. by move: (fx0); rewrite -{1}oppe0 -leeNl => /max_idPr ->. 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