proposition: Lemma Cv_radius_weak_minus : forall (An Bn : nat -> R) (r1 r2 : R), Cv_radius_weak An r1 -> Cv_radius_weak Bn r2 -> Cv_radius_weak (An - Bn)%Rseq (Rmin (Rabs r1) (Rabs r2)).
proof: Proof. intros An Bn r1 r2 RhoA RhoB. assert (Rho'B := proj1 (Cv_radius_weak_opp Bn _) RhoB). unfold Rminus ; apply Cv_radius_weak_plus ; assumption. Qed.
imports: Reals Rpser_def Rpser_def_simpl Rinterval Rsequence_def Rsequence_base_facts Rsequence_subsequence Rsequence_rewrite_facts Rsequence_cv_facts Rsequence_facts Rsequence_bound_facts Rsequence_sums_facts Rpow_facts PeanoNat Lra MyRIneq MyNat MyNNR