proposition: Lemma ncvg_sum : ncvg (fun n => \sum_(i < n) S i) (psum S)%:E.
proof: Proof. set u := (fun n => _); apply: contraPP smS => ncv _. case: (ncvg_mono_bnd (u := u)) => //. by apply/ptsum_homo. by apply/psummable_ptbounded. move=> x cvux; suff xE: x = (psum S) by rewrite xE in cvux. apply/eqP; case: (x =P _) => // /eqP /lt_total /orP[]; last first. + rewrite -lte_fin => /ncvg_gt /(_ cvux) [K /(_ _ (leqnn _))] /=. rewrite ltNge lee_fin (le_trans _ (ger_big_ord_psum _ K)) //. by apply/ler_sum=> /= i _; apply/ler_norm. move=> lt_xS; pose e := psum S - x. have ge0_e: 0 < e by rewrite subr_gt0. case: (sup_adherent ge0_e (summable_sup smS)) => y. case=> /= J ->; rewrite /e /psum (asboolT smS). rewrite opprB addrCA subrr addr0 => lt_xSJ. pose k := \max_(j : J) (val j); have lt_x_uSk: x < u k.+1. apply/(lt_le_trans lt_xSJ); rewrite /u big_ord_mkfset. rewrite (eq_bigr (S \o val)) => /= [j _|]; first by rewrite ger0_norm. apply/big_fset_subset=> // j jJ; rewrite in_fset //. by rewrite (mem_iota _ k.+1) /= add0n ltnS (leq_bigmax (FSetSub jJ)). have /= := ncvg_homo_le ptsum_homo cvux k.+1; rewrite -/(u _). by rewrite lee_fin => /le_lt_trans/(_ lt_x_uSk); rewrite ltxx. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology