proposition: Lemma ge0_psum : 0 <= psum S.
proof: Proof. case/boolP: `[< summable S >] => [|/asboolPn/psum_out ->//]. move/asboolP=> smS; have h := @ger_big_psum [::] _ smS. by rewrite (le_trans _ (h _)) ?big_nil. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology