proposition: Lemma nlimE (u : nat -> R) (l : \bar R) : ncvg u l -> nlim u = l.
proof: Proof. move=> cu; have: (ncvg u (nlim u)). by apply/nlim_ncvg; exists l. by move/(ncvg_uniq cu) => ->. 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