proposition: Lemma Cv_radius_weak_zip_r1 : forall An Bn r, Cv_radius_weak (Rseq_zip An Bn) r -> Cv_radius_weak An (r ^ 2).
proof: Proof. intros An Bn r [B HB] ; exists B ; intros x [i Hi] ; subst. transitivity (gt_abs_pser (Rseq_zip An Bn) r (2 * i)). right ; unfold gt_abs_pser, gt_pser, Rseq_abs, Rseq_mult, Rseq_zip. case (n_modulo_2 (2 * i)) ; intros [p Hp]. assert (Hip : i = p) by lia ; rewrite Hip, pow_mult ; reflexivity. apply False_ind ; lia. apply HB ; exists (2 * i)%nat ; 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