proposition: Lemma dcvgP f : dcvg f -> forall x, exists2 l, (0 <= l <= 1) & ncvg (f^~ x) l%:E.
proof: Proof. move=> cv_f x; case: (dlimP f x) => [l ge0_l le1_l cv|]. by exists l => //; apply/andP; split. by case; case: (cv_f x). Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum