proposition: Lemma desum_eqNy (I : finType) (f : I -> \bar^d R) (P : {pred I}) : (forall i, f i != +oo) -> (\sum_(i | P i) f i == -oo) = [exists i in P, f i == -oo].
proof: Proof. move=> finoo. rewrite dual_sumeE eqe_oppLR /= esum_eqy => [|i]; rewrite ?eqe_oppLR //. by under eq_existsb => i do rewrite eqe_oppLR. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed