proposition: Lemma ncvgB u v lu lv : ncvg u lu%:E -> ncvg v lv%:E -> ncvg (u \- v) (lu - lv)%:E.
proof: Proof. by move=> cu cv; apply/ncvgD/ncvgN_fin. 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