proposition: Lemma Cv_radius_weak_prod_prelim : forall An Bn r1 r2, Cv_radius_weak An r1 -> Cv_radius_weak Bn r2 -> Cv_radius_weak ((An # Bn) / Rseq_shift INR)%Rseq (Rmin (Rabs r1) (Rabs r2)).
proof: Proof. intros An Bn r1 r2 rAn rBn. assert (rAn' : Cv_radius_weak An (Rmin (Rabs r1) (Rabs r2))). apply Cv_radius_weak_le_compat with r1. rewrite Rabs_pos_eq ; [apply Rmin_l | apply Rmin_pos ; apply Rabs_pos]. assumption. assert (rBn' : Cv_radius_weak Bn (Rmin (Rabs r1) (Rabs r2))). apply Cv_radius_weak_le_compat with r2. rewrite Rabs_pos_eq ; [apply Rmin_r | apply Rmin_pos ; apply Rabs_pos]. assumption. clear rAn rBn ; destruct rAn' as [B1 HB1] ; destruct rBn' as [B2 HB2] ; exists (B1 * B2). assert (H1 : Rseq_bound (gt_abs_pser An (Rmin (Rabs r1) (Rabs r2))) B1). intro n ; apply HB1 ; exists n ; unfold gt_abs_pser, Rseq_abs ; rewrite Rabs_Rabsolu ; reflexivity. assert (H2 : Rseq_bound (gt_abs_pser Bn (Rmin (Rabs r1) (Rabs r2))) B2). intro n ; apply HB2 ; exists n ; unfold gt_abs_pser, Rseq_abs ; rewrite Rabs_Rabsolu ; reflexivity. clear HB1 HB2. intros x [n Hn] ; subst. erewrite gt_abs_pser_ext ; [| eapply Rseq_div_simpl]. rewrite gt_abs_pser_mult_compat_r. eapply Rle_trans ; [eapply Rmult_le_compat_r ; [unfold Rseq_abs ; apply Rabs_pos | eapply gt_abs_pser_prod_le_compat] |]. eapply Rle_trans ; [| eapply Rseq_bound_prod ; try eassumption]. right ; unfold Rseq_div, Rdiv, Rseq_mult ; rewrite Rabs_mult. apply Rmult_eq_compat ; [| unfold Rseq_abs ; reflexivity]. symmetry ; apply Rabs_pos_eq. unfold Rseq_prod ; apply Rseq_sum_pos_strong ; intros p p_bd. unfold Rseq_mult ; apply Rmult_le_pos ; apply gt_abs_pser_pos. 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