proposition: Lemma ncvg_abs u lu : ncvg u lu%:E -> ncvg (fun n => `|u n|) `|lu|%:E.
proof: Proof. move=> cu; elim/nbh_finW => e /= gt0_e; case: (cu (B lu e)). move=> K {}cu; exists K=> n /cu; rewrite !inE eclamp_id //. by move/(le_lt_trans (ler_dist_dist _ _)). 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