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