proposition: Lemma Cos_periodic : forall x : IR, Cos (x[+]Two[*]Pi) [=] Cos x.
proof: Proof. intro. transitivity (Cos (x[+]Pi[+]Pi)). apply Cos_wd; rational. astepl ( [--] (Cos (x[+]Pi))). Step_final ( [--][--] (Cos x)). Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos