proposition: Lemma ncvg_leC c u (lu : \bar R) : (forall n, u n <= c) -> ncvg u lu -> (lu <= c%:E)%E.
proof: Proof. by move=> le cu; apply/(@ncvg_le c%:S u)=> //; apply/ncvgC. 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