proposition: Lemma sin_infinite_cv_radius : infinite_cv_radius sin_seq.
proof: Proof. intros r ; apply Rle_Cv_radius_weak_compat with (| exp_seq |)%R. intro n ; unfold sin_seq, exp_seq, Rseq_zip ; case (n_modulo_2 n) ; intros [p Hp]. unfold zero_seq, Rseq_constant ; rewrite Rabs_R0 ; apply Rabs_pos. unfold Rdiv, Rseq_abs ; rewrite Rabs_Rabsolu, Rabs_mult, pow_1_abs, Rmult_1_l ; subst ; right ; reflexivity. rewrite <- Cv_radius_weak_abs ; apply exp_infinite_cv_radius. Qed.
imports: MyReals MyINR MyNNR Rsequence_def Rsequence_facts Rsequence_cv_facts Rsequence_sums_facts Rsequence_base_facts Rsequence_rewrite_facts Rsequence_usual_facts Rsequence_subsequence PeanoNat Lra Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_cv_facts Rpser_radius_facts Rpser_sums Rpser_derivative Rpser_derivative_facts Rfunction_def Functions Rextensionality Rpow_facts Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity