proposition: Lemma nlim_out u : ~ (exists l, ncvg u l) -> nlim u = -oo%E.
proof: Proof. move=> h; rewrite /nlim; case: {-}_ / idP => // p. by case: h; case/asboolP: p => l /asboolP; exists l. 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