proposition: Lemma Sin_plus_der_lft : forall y n, Derivative_n n realline I (F y) (F' y n).
proof: Proof. intro; apply Derivative_n_chain. simpl in |- *; unfold F in |- *. apply Feq_reflexive. apply included_FComp; Included. intro. cut (maps_compacts_into realline realline (FId{+} [-C-]y)); [ intro | apply maps_translation ]. cut (Derivative realline I (FId{+} [-C-]y) [-C-][1]); intros. 2: apply Derivative_wdr with ( [-C-][1]{+} [-C-][0]:PartIR). 2: FEQ. 2: Deriv. apply four_induction with (P := fun n : nat => Derivative realline I (F' y n) (F' y (S n))). simpl in |- *. apply Derivative_wdr with ((Cosine[o]FId{+} [-C-]y) {*} [-C-][1]). FEQ. apply Derivative_comp with realline I; auto. Deriv. simpl in |- *. apply Derivative_wdr with (( {--}Sine[o]FId{+} [-C-]y) {*} [-C-][1]). FEQ. apply Derivative_comp with realline I; auto. Deriv. simpl in |- *. apply Derivative_inv. apply Derivative_wdr with ((Cosine[o]FId{+} [-C-]y) {*} [-C-][1]). FEQ. apply Derivative_comp with realline I; auto. Deriv. simpl in |- *. apply Derivative_wdr with ( {--} (( {--}Sine[o]FId{+} [-C-]y) {*} [-C-][1])). FEQ. apply Derivative_inv. apply Derivative_comp with realline I; auto. Deriv. intros. auto. Qed.
imports: CoRN.transc.TaylorSeries Coq(Lia)