proposition: Lemma Cv_radius_weak_zip_r2 : forall An Bn r, Cv_radius_weak (Rseq_zip An Bn) r -> Cv_radius_weak Bn (r ^ 2).
proof: Proof. intros An Bn r [B HB] ; destruct (Req_dec (Rabs r) 0) as [r_eq | r_neq]. rewrite (Rabs_null_rev _ r_eq) ; simpl ; rewrite Rmult_0_l ; apply Cv_radius_weak_0. exists (B / Rabs r) ; intros x [i Hi] ; subst. transitivity (gt_abs_pser (Rseq_zip An Bn) r (S (2 * i)) / Rabs r). right ; unfold gt_abs_pser, gt_pser, Rseq_abs, Rseq_mult, Rseq_zip. case (n_modulo_2 (S (2 * i))) ; intros [p Hp]. apply False_ind ; lia. assert (Hip : i = p) by lia ; rewrite Hip , <- pow_mult, <- tech_pow_Rmult. replace (Bn p * (r * r ^ (2 * p))) with (Bn p * r ^ (2 * p) * r) by ring. unfold Rdiv ; rewrite (Rabs_mult _ r), Rmult_assoc, Rinv_r, Rmult_1_r. reflexivity. assumption. apply Rmult_le_compat_r. left ; apply Rinv_0_lt_compat, Rabs_pos_lt, Rabs_neq_rev ; assumption. apply HB ; exists (S (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