proposition: Lemma Cv_radius_weak_Cnorm_compat_rev : forall (An : nat -> C) (r : R), Cv_radius_weak (fun n => Cnorm (An n)) r -> Cv_radius_weak An r.
proof: Proof. intros An r [M HM] ; exists M. intros x [n Hn] ; rewrite Hn. unfold_gt ; rewrite Cnorm_Cmult, <- Cnorm_invol, <- Cnorm_Cmult ; 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