proposition: Lemma Cos_ap_Zero : forall x:IR, (forall z, x[#]Pi[/]TwoNZ[+](zring z)[*]Pi) -> Cos x [#] [0].
proof: Proof. intros x Hx. stepl (Cos (x[-](Pi[/]TwoNZ)[+](Pi[/]TwoNZ))); [| now apply Cos_wd; rational]. csetoid_rewrite (Cos_plus_HalfPi (x[-](Pi[/]TwoNZ))). rstepr ([--][0]:IR). apply inv_resp_ap. apply Sin_ap_Zero. intros i. apply zero_minus_apart. rstepl (x[-](Pi[/]TwoNZ[+]zring i[*]Pi)). apply minus_ap_zero. apply Hx. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac