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