proposition: Lemma esum_eqy (I : finType) (P : {pred I}) (f : I -> \bar R) : (forall i, P i -> f i != -oo) -> (\sum_(i | P i) f i == +oo) = [exists i in P, f i == +oo].
proof: Proof. move=> fio; apply/idP/existsP => [/eqP /=|[/= i /andP[Pi /eqP fi]]]. have {}fio : (forall i, P i -> f i != -oo) by move=> i Pi; exact: fio. by move=> /(esum_eqyP _ fio)[i [_ Pi fi]]; exists i; rewrite fi eqxx andbT. by apply/eqP/esum_eqyP => //; exists i. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed