proposition: Lemma desum_eqNyP (T : eqType) (s : seq T) (P : pred T) (f : T -> \bar^d 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=> fioo. rewrite dual_sumeE eqe_oppLRP /= esum_eqyP => [|i Pi]; last first. by rewrite eqe_oppLR fioo. by split=> -[i + /ltac:(exists i)] => [|] []; [|split]; rewrite // eqe_oppLRP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed