proposition: Lemma Tang_Domain : forall x:IR, (forall z, x[#]Pi[/]TwoNZ[+](zring z)[*]Pi) -> Dom Tang x.
proof: Proof. intros. repeat split; try constructor. intros []. apply: Cos_ap_Zero. assumption. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac