proposition: Lemma cvg_nseries_near (u : nat^nat) : cvgn (nseries u) -> \forall n \near \oo, u n = 0%N.
proof: Proof. move=> /cvg_ex[l ul]; have /ul[a _ aul] : nbhs l [set l]. by exists [set l]; split=> //; exists [set l] => //; rewrite bigcup_set1. have /ul[b _ bul] : nbhs l [set l.-1; l]. by exists [set l]; split => //; exists [set l] => //; rewrite bigcup_set1. exists (maxn a b) => // n /= abn. rewrite (_ : u = fun n => nseries u n.+1 - nseries u n)%N; last first. by rewrite funeqE => i; rewrite /nseries big_nat_recr//= addnC addnK. have /aul -> : (a <= n)%N by rewrite (leq_trans _ abn) // leq_max leqnn. have /bul[->|->] : (b <= n.+1)%N by rewrite leqW// (leq_trans _ abn)// leq_maxr. - by apply/eqP; rewrite subn_eq0// leq_pred. - by rewrite subnn. 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