proposition: Lemma Sin_Pi : Sin Pi [=] [0].
proof: Proof. transitivity (Sin (Pi [/]TwoNZ[+]Pi [/]TwoNZ)). apply Sin_wd; rational. eapply eq_transitive_unfolded. apply Sin_plus_HalfPi. algebra. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos