proposition: Lemma ncvg_eq v u l : u =1 v -> ncvg v l -> ncvg u l.
proof: Proof. by move=> eq; apply: (@ncvg_eq_from 0). 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