proposition: Lemma ncvg_sub h u lu : {homo h : x y / (x < y)%N} -> ncvg u lu -> ncvg (fun n => u (h n)) lu.
proof: Proof. move=> mono_h cvu v; case: (cvu v)=> K {}cvu; exists K. move=> n le_Kn; apply/cvu; apply/(leq_trans le_Kn). elim: {le_Kn} n => [|n ih] //; apply/(leq_ltn_trans ih). by rewrite mono_h. 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