proposition: Lemma Sin_plus_Pi : forall x : IR, Sin (x[+]Pi) [=] [--] (Sin x).
proof: Proof. intros. transitivity (Sin (x[+]Pi [/]TwoNZ[+]Pi [/]TwoNZ)). apply Sin_wd; rational. eapply eq_transitive. apply Sin_plus_HalfPi. apply Cos_plus_HalfPi. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos