proposition: Lemma Deriv_sin_seq_simpl : (An_deriv sin_seq == cos_seq)%Rseq.
proof: Proof. intro n ; unfold cos_seq, sin_seq, An_deriv, Rseq_shift, Rseq_mult, Rseq_zip, zero_seq, Rseq_constant ; case (n_modulo_2 n) ; intros [p Hp] ; case (n_modulo_2 (S n)) ; intros [q Hq]. apply False_ind ; lia. rewrite <- Hq ; replace q with p by lia ; rewrite <- Hp. rewrite Rmult_comm ; unfold Rdiv ; rewrite Rmult_assoc. replace (/ INR (fact (S n)) * INR (S n)) with (/ INR (fact n)). simpl ; ring. rewrite fact_simpl, mult_INR ; field ; split ; apply not_0_INR ; [apply fact_neq_0 | intuition]. ring. apply False_ind ; lia. 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