proposition: Lemma leub_dlim f mu : (forall n, f n <=1 mu) -> dlim f <=1 mu.
proof: Proof. move=> le x; apply/(@le_trans _ _ ((\dlim_(n) mu) x)). by apply/le_dlim => // y; exists (mu y)%:E; apply/ncvgC. by rewrite dlimE nlimC. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum