proposition: Lemma psummable_ptbounded : nbounded (fun n => \sum_(i < n) S i).
proof: Proof. apply/asboolP/nboundedP; exists (psum S + 1). rewrite ltr_pwDr ?ltr01 1?(le_trans (normr_ge0 (S 0%N))) //. by apply/ger1_psum. move=> n; rewrite ltr_pwDr ?ltr01 // ger0_norm ?sumr_ge0 //. apply/(le_trans _ (ger_big_ord_psum _ n)) => //. by apply/ler_sum=> /= i _; apply/ler_norm. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology