proposition: Lemma Sin_inv : forall x : IR, Sin [--]x [=] [--] (Sin x).
proof: Proof. intros. simpl in |- *. assert (H : forall (x : nat -> IR) (convX : convergent x), series_sum _ (conv_series_inv _ convX) [=] [--] (series_sum x convX)). intros; apply series_sum_inv. eapply eq_transitive_unfolded. 2: apply H. apply series_sum_wd. intro. unfold sin_seq in |- *. elim even_or_odd_plus; intros; simpl in |- *. elim p; intros; simpl in |- *. rational. apply eq_transitive_unfolded with ( [--][1][^]x0[*] ( [--]x[-][0]) [^]n[/] _[//]nring_fac_ap_zero IR n). simpl in |- *; rational. apply eq_transitive_unfolded with ( [--][1][^]x0[*][--] ((x[-][0]) [^]n) [/] _[//]nring_fac_ap_zero IR n). 2: simpl in |- *; rational. apply div_wd. 2: algebra. apply mult_wdr. rewrite b. eapply eq_transitive_unfolded. 2: apply inv_nexp_odd; apply Nat.Odd_succ; apply even_plus_n_n. apply nexp_wd; rational. Qed.
imports: CoRN.transc.Trigonometric