proposition: Lemma Cv_radius_weak_opp : forall (An : nat -> C) (r : R), Cv_radius_weak An r -> Cv_radius_weak (fun n => - An n) r.
proof: Proof. intros An r Rho. destruct Rho as (C, HC) ; exists C ; intros x Hx ; destruct Hx as (u,Hu) ; rewrite Hu ; unfold_gt ; rewrite Copp_mult_distr_l_reverse ; rewrite Cnorm_opp ; apply HC ; exists u ; intuition. Qed.
imports: Rsequence_def Rpser_def Rpow_facts Cmet Cnorm Ctacfield Cpow Cprop_base Csequence_def Csequence_facts Cpser_def Lia