proposition: Lemma nlimD (u v : nat -> R) : iscvg u -> iscvg v -> nlim (u \+ v) = (nlim u + nlim v)%E.
proof: Proof. case=> [lu cu] [lv cv]; rewrite (nlimE cu) (nlimE cv) /=. by rewrite (nlimE (ncvgD cu cv)). 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