proposition: Lemma esum_eqNyP (T : eqType) (s : seq T) (P : pred T) (f : T -> \bar R) : \sum_(i <- s | P i) f i = -oo <-> exists i, [/\ i \in s, P i & f i = -oo].
proof: Proof. 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. rewrite big_mkcond (bigID (xpred1 i))/= (eq_bigr (fun _ => -oo)); last first. by move=> j /eqP ->; rewrite Pi. rewrite big_const_seq/= [X in X + _](_ : _ = -oo)//. elim: s i Pi fi si => // h t ih i Pi fi. rewrite inE => /predU1P[<-/=|it]; first by rewrite eqxx. by rewrite /= iterD ih//=; case: (_ == _). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed