proposition: Lemma Cos_plus_fun : forall y, Feq realline (Cosine[o]FId{+} [-C-]y) (Cosine{*} [-C-] (Cos y) {-}Sine{*} [-C-] (Sin y)).
proof: Proof. intro. assert (H : Derivative realline I Sine Cosine). Deriv. assert (H0 : Derivative realline I Cosine {--}Sine). Deriv. apply Derivative_unique with I (Sine[o]FId{+} [-C-]y). Derivative_Help. FEQ. apply Derivative_comp with realline I. apply maps_translation. Deriv. Deriv. apply Derivative_wdl with (Sine{*} [-C-] (Cos y) {+}Cosine{*} [-C-] (Sin y)). apply Feq_symmetric; apply Sin_plus_fun. apply Derivative_wdl with (Cos y{**}Sine{+}Sin y{**}Cosine). apply eq_imp_Feq. apply included_FPlus; Included. apply included_FPlus; Included. intros; simpl in |- *; rational. apply Derivative_wdr with (Cos y{**}Cosine{+}Sin y{**}{--}Sine). apply eq_imp_Feq. apply included_FPlus; Included. apply included_FMinus; Included. intros; simpl in |- *; rational. Deriv. Qed.
imports: CoRN.transc.TaylorSeries Coq(Lia)