proposition: Lemma Cv_radius_weak_Cnorm_compat2 : forall (An : nat -> C) (r : R), Cv_radius_weak An r -> Rpser_def.Cv_radius_weak (fun n => Cnorm (An n)) r.
proof: Proof. intros An r Rho. elim Rho ; intros m Hm ; exists m ; unfold_gt ; unfold gt_abs_pser, Rpser_def.gt_pser, Rseq_abs, Rseq_mult ; intros a Ha ; unfold EUn in Ha ; elim Ha ; intros u Hu ; rewrite Hu ; rewrite Rabs_mult ; do 2 rewrite <- Cnorm_IRC_Rabs ; rewrite Cnorm_invol, <- Cnorm_Cmult ; apply Hm. exists u ; unfold_gt ; rewrite IRC_pow_compat ; reflexivity. Qed.
imports: Rsequence_def Rpser_def Rpow_facts Cmet Cnorm Ctacfield Cpow Cprop_base Csequence_def Csequence_facts Cpser_def Lia