proposition: Lemma sine_eq_Deriv_cosine : forall x, sine x = - Deriv_cosine x.
proof: Proof. intro x. assert (T1 := sum_sums _ sin_infinite_cv_radius x) ; assert (T2 := sum_derive_sums _ cos_infinite_cv_radius x). symmetry ; apply Rpser_unique_extentionality with (- An_deriv cos_seq)%Rseq (sin_seq) x. intro n ; rewrite <- Ropp_involutive ; apply Ropp_eq_compat ; apply Deriv_cos_seq_simpl. apply Rpser_opp_compat ; apply T2. apply T1. 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