proposition: Lemma ncvg_eq_from K v u l : (forall n, (K <= n)%N -> u n = v n) -> ncvg v l -> ncvg u l.
proof: Proof. move=> eq cu nb; case: (cu nb) => Ku {}cu; exists (maxn K Ku) => n. by rewrite geq_max => /andP[leK leKu]; rewrite eq // cu. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.bigenough.bigenough mathcomp.classical(boolp classical_sets functions) mathcomp.classical(mathcomp_extra) xfinmap ereal reals discrete topology