proposition: Lemma esum_pred_image (R : realType) (T : choiceType) (a : T -> \bar R) (e : nat -> T) (P : pred nat) : (forall n, P n -> 0 <= a (e n)) -> set_inj P e -> \esum_(i in e @` P) a i = \sum_(i <oo | P i) a (e i).
proof: Proof. by move=> a0 einj; rewrite esum_image// nneseries_esum. 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