proposition: Lemma eq_from_nlim K (v u : nat -> R) : (forall n, (K <= n)%N -> u n = v n) -> nlim u = nlim v.
proof: Proof. move=> eq; have h := ncvg_eq_from eq; case: (nlimP v). by move=> l cv; have cu := h _ cv; rewrite (nlimE cu). move=> Ncv; rewrite nlim_out //; case=> l cu. apply: Ncv; exists l; apply/(@ncvg_eq_from _ K u) => //. by move=> n /eq /esym. 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