proposition: Lemma Sin_plus_der_rht : forall y n, Derivative_n n realline I (G y) (G' y n).
proof: Proof. intro; apply Derivative_n_chain. simpl in |- *; unfold G in |- *. apply Feq_reflexive. apply included_FPlus; Included. intro. cut (Derivative realline I Sine Cosine); [ intro | Deriv ]. cut (Derivative realline I Cosine {--}Sine); [ intro | Deriv ]. apply four_induction with (P := fun n : nat => Derivative realline I (G' y n) (G' y (S n))). simpl in |- *. let r := PartIR_to_symbPF (Sine{*} [-C-] (Cos y) {+}Cosine{*} [-C-] (Sin y)) in apply Derivative_wdr with (symbPF_deriv r). simpl in |- *. apply eq_imp_Feq. repeat split. repeat split. intros; simpl in |- *; rational. simpl in |- *; Deriv. simpl in |- *. let r := PartIR_to_symbPF (Cosine{*} [-C-] (Cos y) {-}Sine{*} [-C-] (Sin y)) in apply Derivative_wdr with (symbPF_deriv r). simpl in |- *. apply eq_imp_Feq. repeat split. repeat split. intros; simpl in |- *; rational. simpl in |- *; Deriv. simpl in |- *. let r := PartIR_to_symbPF ( {--} (Sine{*} [-C-] (Cos y) {+}Cosine{*} [-C-] (Sin y))) in apply Derivative_wdr with (symbPF_deriv r). simpl in |- *. apply eq_imp_Feq. repeat split. repeat split. intros; simpl in |- *; rational. simpl in |- *; Deriv. simpl in |- *. let r := PartIR_to_symbPF (Sine{*} [-C-] (Sin y) {-}Cosine{*} [-C-] (Cos y)) in apply Derivative_wdr with (symbPF_deriv r). simpl in |- *. apply eq_imp_Feq. repeat split. repeat split. intros; simpl in |- *; rational. simpl in |- *; Deriv. auto. Qed.
imports: CoRN.transc.TaylorSeries Coq(Lia)