proposition: Lemma cos_cosine : cos == cosine.
proof: Proof. intro x ; eapply Rpser_unique, sum_sums. unfold cos ; destruct (exist_cos (x²)) as [la Hla]. apply Rpser_zip_compat_0_l. unfold Rpser ; rewrite Rseq_cv_eq_compat. apply Hla. apply Rseq_sum_ext ; intro n ; unfold gt_pser, Rseq_mult, cos_n. rewrite <- pow_Rsqr, pow_mult ; reflexivity. 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