proposition: Lemma Derivative_Cos : forall H, Derivative realline H Cosine {--}Sine.
proof: Proof. intro. unfold Sine, Cosine, sin_ps, cos_ps in |- *. cut (fun_series_convergent_IR realline (FPowerSeries' [0] (fun n : nat => cos_seq (S n)))). intro H0. eapply Derivative_wdr. 2: apply Derivative_FPowerSeries1' with (Hg := H0). FEQ. simpl in |- *. apply eq_transitive_unfolded with (series_sum _ (conv_series_inv _ (fun_series_conv_imp_conv _ _ (leEq_reflexive _ x) _ (sin_conv _ _ (leEq_reflexive _ x) (compact_single_iprop realline x Hx')) x (compact_single_prop x) (fun_series_inc_IR realline _ sin_conv x Hx')))). apply series_sum_wd; intros. simpl in |- *. rstepr (( [--] (sin_seq n) [/] _[//]nring_fac_ap_zero _ n) [*]nexp IR n (x[-][0])). apply mult_wdl. apply div_wd. apply eq_symmetric_unfolded. astepr ( [--][--] (cos_seq (S n))); apply un_op_wd_unfolded. apply sin_cos_seq. algebra. simpl in |- *. apply series_sum_inv with (x := fun n : nat => (sin_seq n[/] _[//]nring_fac_ap_zero IR n) [*]nexp IR n (x[-][0])). apply fun_series_convergent_wd_IR with (fun n : nat => {--} (FPowerSeries' [0] sin_seq n)). intros; FEQ. repeat split. repeat split. simpl in |- *. rstepl (( [--] (sin_seq n) [/] _[//]nring_fac_ap_zero _ n) [*]nexp IR n (x[-][0])). apply mult_wdl. apply div_wd. astepr ( [--][--] (cos_seq (S n))); apply un_op_wd_unfolded. apply sin_cos_seq. algebra. apply FSeries_Sum_inv_conv. apply sin_conv. Qed.
imports: CoRN.transc.TaylorSeries Coq(Lia)