proposition: Lemma le_dlim f g : (forall n, f n <=1 g n) -> dcvg g -> dlim f <=1 dlim g.
proof: Proof. move=> le dcvg_g x; case: dlimP => [|_]; last by apply/ge0_dlim. move=> l _ _ h; case: dlimP => [l' _ _ h'|]; last by case. by rewrite -lee_fin; apply/(ncvg_le _ h' h). Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum