proposition: Lemma lte_sum_pinfty I (s : seq I) (P : pred I) (f : I -> \bar R) : (forall i, P i -> f i < +oo) -> \sum_(i <- s | P i) f i < +oo.
proof: Proof. elim/big_ind : _ => [_|x y xoo yoo foo|i ?]; [exact: ltry| |exact]. by apply: lte_add_pinfty; [exact: xoo| exact: yoo]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed