proposition: Lemma ncvgC c : ncvg c%:S c%:E.
proof: Proof. elim/nbh_finW => e /= gt0_e; exists 0%N => n _. by rewrite inE subrr normr0. 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