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