proposition: Lemma eq_from_dlim K f g : (forall n, (K <= n)%N -> f n =1 g n) -> dlim f =1 dlim g.
proof: Proof. move=> eq_fg x; rewrite !dlimE; congr (_ _). by apply/(eq_from_nlim (K := K)); move=> n /eq_fg /(_ x). Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum