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