proposition: Lemma Cv_radius_weak_0 : forall An, Cv_radius_weak An 0.
proof: Proof. intro An ; exists (Cnorm (An O)) ; intros x [n Hn] ; rewrite Hn ; unfold_gt ; destruct n. rewrite Cpow_0 ; right ; apply Cnorm_eq_compat ; intuition (auto with complex). rewrite IRC_pow_compat, pow_i, Cmult_0_r, Cnorm_C0 ; [apply Cnorm_pos | intuition (auto with arith)]. Qed.
imports: Rsequence_def Rpser_def Rpow_facts Cmet Cnorm Ctacfield Cpow Cprop_base Csequence_def Csequence_facts Cpser_def Lia