proposition: Lemma esum_eqyP (T : eqType) (s : seq T) (P : pred T) (f : T -> \bar R) : (forall i, P i -> f i != -oo) -> \sum_(i <- s | P i) f i = +oo <-> exists i, [/\ i \in s, P i & f i = +oo].
proof: Proof. move=> finoo; split=> [|[i [si Pi fi]]]. rewrite big_seq_cond; elim/big_ind: _ => // [[?| |] [?| |]//|]. by move=> i /andP[si Pi] fioo; exists i; rewrite si Pi fioo. elim: s i Pi fi si => // h t ih i Pi fi. rewrite inE => /predU1P[<-/=|it]. rewrite big_cons Pi fi addye//. by apply/eqP => /esum_eqNyP[j [jt /finoo/negbTE/eqP]]. by rewrite big_cons; case: ifPn => Ph; rewrite (ih i)// addey// finoo. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed