proposition: Lemma lt_psum (F : T -> R) l : summable F -> l < psum F -> exists J : {fset T}, l < \sum_(j : J) `|F (val j)|.
proof: Proof. move=> smF; rewrite /psum (asboolT smF) => /lt_sup_imfset. by case=> /= [|J lt_lJ _]; [apply/summable_sup | exists J]. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology