proposition: Lemma iscvg_eq (u v : nat -> R) : u =1 v -> iscvg v -> iscvg u.
proof: Proof. by move=> equv [l h]; exists l; apply/(ncvg_eq equv). 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