proposition: Lemma Cv_radius_weak_minus : forall (An Bn : nat -> C) (r1 r2 : R), Cv_radius_weak An r1 -> Cv_radius_weak Bn r2 -> Cv_radius_weak (fun n => An n - Bn n) (Rmin (Rabs r1) (Rabs r2)).
proof: Proof. intros An Bn r1 r2 RhoA RhoB. assert (Rho'B := Cv_radius_weak_opp Bn _ RhoB). unfold Rminus ; apply Cv_radius_weak_plus ; assumption. Qed.
imports: Rsequence_def Rpser_def Rpow_facts Cmet Cnorm Ctacfield Cpow Cprop_base Csequence_def Csequence_facts Cpser_def Lia