proposition: Lemma Cv_radius_weak_Cnorm_compat_rev2 : forall (An : nat -> C) (r : R), Rpser_def.Cv_radius_weak (fun n => Cnorm (An n)) r -> Cv_radius_weak An r.
proof: Proof. intros An r [M HM] ; apply Cv_radius_weak_Cnorm_compat_rev ; exists M ; intros x [n Hn] ; rewrite Hn ; unfold_gt ; rewrite Cnorm_Cmult, IRC_pow_compat ; do 2 rewrite Cnorm_IRC_Rabs ; rewrite <- Rabs_mult ; apply HM ; exists n ; reflexivity. Qed.
imports: Rsequence_def Rpser_def Rpow_facts Cmet Cnorm Ctacfield Cpow Cprop_base Csequence_def Csequence_facts Cpser_def Lia