proposition: Lemma dcvg_homo f : (forall n m, (n <= m)%N -> f n <=1 f m) -> dcvg f.
proof: Proof. move=> mn_f x; have: forall n m, (n <= m)%N -> f n x <= f m x. by move=> n m /mn_f; apply. case/ncvg_mono_bnd => {mn_f}; first apply/asboolP/nboundedP. exists 2%:R => // n; apply/(@le_lt_trans _ _ 1%:R)/ltr_nat. by rewrite ger0_norm // le1_mu1. by move=> y h; exists y%:E. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum