proposition: Lemma Sin_plus_HalfPi : forall x : IR, Sin (x[+]Pi [/]TwoNZ) [=] Cos x.
proof: Proof. intro. eapply eq_transitive. apply Sin_plus. astepl (Sin x[*][0][+]Cos x[*][1]). Step_final ([0][+]Cos x). Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos