proposition: Lemma integralN D (f : T -> \bar R) : \int[mu]_(x in D) f^\+ x +? (- \int[mu]_(x in D) f^\- x) -> \int[mu]_(x in D) - f x = - \int[mu]_(x in D) f x.
proof: Proof. have [f_fin _|] := boolP (\int[mu]_(x in D) f^\- x \is a fin_num). rewrite integralE// [in RHS]integralE// fin_num_oppeD ?fin_numN// oppeK addeC. by rewrite funenegN. rewrite fin_numE negb_and 2!negbK => /orP[nfoo|/eqP nfoo]. exfalso; move/negP : nfoo; apply; rewrite -leeNy_eq; apply/negP. by rewrite -ltNge (lt_le_trans _ (integral_ge0 _ _)). rewrite nfoo adde_defEninfty -leye_eq -ltNge ltey_eq => /orP[f_fin|/eqP pfoo]. rewrite integralE [in RHS]integralE nfoo [in RHS]addeC/= funenegN. by rewrite addye// eqe_oppLR/= (andP (eqbLR (fin_numE _) f_fin)).2. by rewrite integralE// [in RHS]integralE// funeposN funenegN nfoo pfoo. 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