proposition: Lemma eq_nlim (v u : nat -> R) : u =1 v -> nlim u = nlim v.
proof: Proof. by move=> eq; apply/(@eq_from_nlim 0) => n _; apply/eq. 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