proposition: Lemma nneseries_tail_cvg (R : realType) (f : (\bar R)^nat) : \sum_(k <oo) f k < +oo -> (forall k, 0 <= f k) -> \sum_(N <= k <oo) f k @[N --> \oo] --> 0.
proof: Proof. move=> foo f0. have : cvg (\sum_(0 <= k < n) f k @[n --> \oo]). by apply: ereal_nondecreasing_is_cvgn; exact: lee_sum_nneg_natr. move/cvg_ex => [[l fl||/cvg_lim fnoo]] /=; last 2 first. - by move/cvg_lim => fpoo; rewrite fpoo// in foo. - have : 0 <= \sum_(k <oo) f k by exact: nneseries_ge0. by rewrite fnoo. rewrite [X in X @ _ --> _](_ : _ = fun N => l%:E - \sum_(0 <= k < N) f k). apply/cvgeNP; rewrite oppe0. under eq_fun => ? do rewrite oppeD// oppeK addeC. exact/cvge_sub0. apply/funext => N; apply/esym/eqP; rewrite sube_eq//. by rewrite addeC big_mkord -(nneseries_split N)//; exact/eqP/esym/cvg_lim. by rewrite ge0_adde_def//= ?inE; [exact: nneseries_ge0|exact: sume_ge0]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau