proposition: Lemma nlim_ncvg u : (exists l, ncvg u l) -> ncvg u (nlim u).
proof: Proof. case=> l cv_u_l; rewrite /nlim; case: {-}_ / idP; last first. by case; apply/asboolP; exists l; apply/asboolP. by move=> p; apply/asboolP/(xchooseP (asboolP _ p)). 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