proposition: Lemma Sin_HalfPi_minus : forall x : IR, Sin (Pi [/]TwoNZ[-]x) [=] Cos x.
proof: Proof. intros. unfold cg_minus in |- *. astepl (Sin ( [--]x[+]Pi [/]TwoNZ)). eapply eq_transitive. apply Sin_plus_HalfPi. algebra. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos