proposition: Lemma Derivative_Sin : forall H, Derivative realline H Sine Cosine.
proof: Proof. intro. unfold Sine, Cosine, sin_ps, cos_ps in |- *. cut (fun_series_convergent_IR realline (FPowerSeries' [0] (fun n : nat => sin_seq (S n)))). intro H0. eapply Derivative_wdr. 2: apply Derivative_FPowerSeries1' with (Hg := H0). FEQ. simpl in |- *. apply series_sum_wd; intros. apply mult_wdl. apply div_wd. apply eq_symmetric_unfolded; apply cos_sin_seq. algebra. apply fun_series_convergent_wd_IR with (FPowerSeries' [0] cos_seq). intros; FEQ. repeat split. repeat split. simpl in |- *. apply mult_wdl. apply div_wd. apply cos_sin_seq. algebra. apply cos_conv. Qed.
imports: CoRN.transc.TaylorSeries Coq(Lia)