proposition: Lemma desum_eqy (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. rewrite dual_sumeE eqe_oppLR esum_eqNy. by under eq_existsb => i do rewrite eqe_oppLR. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed