proposition: Lemma nlimP u : nlim_spec u (nlim u).
proof: Proof. case/boolP: `[< exists l, `[< ncvg u l >] >] => /asboolP/exists_asboolP/asboolP. by move/nlim_ncvg=> h; apply/NLimCvg. by move=> h; rewrite nlim_out //; apply/NLimOut. 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