proposition: Lemma iscvg_sub σ u : {homo σ : x y / (x < y)%N} -> iscvg u -> iscvg (u \o σ).
proof: Proof. by move=> homoσ [l h]; exists l; apply/ncvg_sub. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.bigenough.bigenough mathcomp.classical(boolp classical_sets functions) mathcomp.classical(mathcomp_extra) xfinmap ereal reals discrete topology