proposition: Lemma dlim_ub f k : (forall n m, (n <= m)%N -> f n <=1 f m) -> f k <=1 dlim f.
proof: Proof. move=> mn_f x; rewrite dlimE -lee_fin; pose u n := f n x. apply/(ncvg_homo_le (u := u))=> [m n /mn_f|]; first by apply. move/dcvg_homo: mn_f => /dcvgP /(_ x) [l _]. by move=> cv; rewrite (nlimE cv). Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum