proposition: Lemma diff_equa_sin : forall (rc : infinite_cv_radius sin_seq), forall x, nth_derive (sum _ rc) (D_infty_Rpser _ rc 2%nat) x = - nth_derive (sum _ rc) (D_infty_Rpser _ rc O) x.
proof: Proof. intro rc ; solve_diff_equa ; intro n ; rewrite An_nth_deriv_S', An_nth_deriv_1, (An_deriv_ext _ cos_seq) ; [apply Deriv_cos_seq_simpl | apply Deriv_sin_seq_simpl]. Qed.
imports: Rsequence_def Rsequence_base_facts Reals Rfunction_def Rfunction_facts Rextensionality Nth_derivative_def Nth_derivative_facts Rpser Rfunction_classes Dequa_def Dequa_facts Dequa_quote List