proposition: Lemma Cv_radius_weak_opp : forall (An : Rseq) (r : R), Cv_radius_weak An r <-> Cv_radius_weak (- An)%Rseq r.
proof: Proof. intros An r ; split ; intros [B HB] ; exists B ; intros x [i Hi] ; subst ; unfold gt_abs_pser, gt_pser, Rseq_abs, Rseq_mult. unfold Rseq_opp ; rewrite Ropp_mult_distr_l_reverse, Rabs_Ropp ; apply HB ; exists i ; reflexivity. rewrite <- Rabs_Ropp, <- Ropp_mult_distr_l_reverse ; apply HB ; exists i ; reflexivity. 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