proposition: Lemma Cos_inv : forall x : IR, Cos [--]x [=] Cos x.
proof: Proof. intros. simpl in |- *. apply series_sum_wd. intro. unfold cos_seq in |- *. elim even_or_odd_plus; intros; simpl in |- *. elim p; intros; simpl in |- *. 2: rational. apply mult_wdr. astepl (( [--]x[-][0]) [^]n); astepr ((x[-][0]) [^]n). rewrite a. eapply eq_transitive_unfolded. 2: apply inv_nexp_even; apply even_plus_n_n. apply nexp_wd; rational. Qed.
imports: CoRN.transc.Trigonometric