proposition: Lemma dlimP f x : dlim_spec f x (dlim f x).
proof: Proof. rewrite dlimE; case: nlimP => [l h|?] /=; last by apply/DLimOut. have: (0%:E <= l)%E by apply/ncvg_geC: h => n; apply/ge0_mu. have: (l <= 1%:E)%E by apply/ncvg_leC: h => n; apply/le1_mu1. by case: l h => // l h /= ge0_l ge1_; apply/DLimCvg. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum