proposition: Lemma Cos_Pi : Cos Pi [=] [--][1].
proof: Proof. transitivity (Cos (Pi [/]TwoNZ[+]Pi [/]TwoNZ)). apply Cos_wd; rational. eapply eq_transitive. apply Cos_plus_HalfPi. algebra. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos