proposition: Lemma C_cos_sin : forall n, C n sin * C n cos * C n (-sin)%F * C n (-cos)%F.
proof: Proof. intro n ; induction n. repeat split; constructor; reg. destruct IHn as [[[IHs IHc] IHns] IHnc]. repeat split. apply C_S with derivable_sin. apply C_ext with cos. intro x ; symmetry ; unfold derive ; reg. assumption. apply C_S with derivable_cos. apply C_ext with (-sin)%F. intro x ; symmetry ; unfold derive ; reg. assumption. assert (dns : derivable (-sin)) by reg. apply C_S with dns. apply C_ext with (-cos)%F. intro x ; symmetry ; unfold derive ; reg. assumption. assert (dnc : derivable (-cos)) by reg. apply C_S with dnc. apply C_ext with sin. intro x ; symmetry ; unfold derive ; reg. assumption. Qed.
imports: Reals Rsequence_def Rfunction_facts Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rfunction_classes_def Rfunction_classes_facts Rextensionality Rpser_def Rpser_def Rpser_cv_facts Rpser_sums Rpser_sums_facts Rpser_derivative