proposition: Lemma Cv_radius_weak_expand_compat : forall An r l, Cv_radius_weak An (l * r) <-> Cv_radius_weak (An_expand An l) r.
proof: Proof. intros An r l ; split ; intros [B HB] ; exists B ; intros x [i Hi] ; subst ; apply HB ; exists i ; unfold An_expand, gt_abs_pser, gt_pser, Rseq_mult, Rseq_abs, Rseq_pow ; apply Rabs_eq_compat ; rewrite Rpow_mult_distr ; ring. 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