proposition: Lemma psum_out S : ~ summable S -> psum S = 0.
proof: Proof. by move/asboolPn/negbTE=> smN; rewrite /psum smN. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology