proposition: Lemma desum_eqyP (T : eqType) (s : seq T) (P : pred T) (f : T -> \bar^d R) : \sum_(i <- s | P i) f i = +oo <-> exists i, [/\ i \in s, P i & f i = +oo].
proof: Proof. rewrite dual_sumeE eqe_oppLRP /= esum_eqNyP. by split=> -[i + /ltac:(exists i)] => [|] []; [|split]; rewrite // eqe_oppLRP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed