proposition: Lemma summable_eseries_esum (f : nat -> \bar R) (P : pred nat) : summable P f -> \sum_(i <oo | P i) f i = esum P f^\+ - esum P f^\-.
proof: Proof. move=> Pfoo; rewrite -nneseries_esum; last first. by move=> n Pn; rewrite /maxe; case: ifPn => //; rewrite -leNgt. rewrite -nneseries_esum ?[LHS]summable_eseries//. by move=> n Pn; rewrite /maxe; case: ifPn => //; rewrite leNgt. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology sequences normedtype numfun