proposition: Lemma Cos_periodic_Z : forall (x : IR) z, Cos (x[+]zring z[*](Two[*]Pi)) [=] Cos x.
proof: Proof. intros x z; revert x; induction z using Zind; intros x. rational. unfold Z.succ. rewrite -> zring_plus. rstepl (Cos (x[+]zring z[*](Two[*]Pi)[+]Two[*]Pi)). rewrite -> Cos_periodic. auto. unfold Z.pred. rewrite -> zring_plus. rstepl (Cos (x[-]Two[*]Pi[+]zring z[*](Two[*]Pi))). rstepr (Cos (x[-]Two[*]Pi[+]Two[*]Pi)). rewrite -> Cos_periodic. auto. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos