proposition: Lemma Tang_Domain' : included (olor ([--](Pi[/]TwoNZ)) (Pi[/]TwoNZ)) (Dom Tang).
proof: Proof. intros x [Hx0 Hx1]. apply Tang_Domain. intros z. destruct (Z_lt_le_dec z 0). apply Greater_imp_ap. eapply leEq_less_trans;[|apply Hx0]. rstepr ([--][0][*]Pi[-]Pi[/]TwoNZ). apply shift_leEq_minus. rstepl (((zring z)[+](zring 1))[*]Pi). apply mult_resp_leEq_rht;[|apply less_leEq; auto with *]. stepl (zring (z+1):IR); [| now apply zring_plus]. replace (z+1)%Z with (-(-z-1))%Z by ring. assert (0<=-z-1)%Z. auto with *. rewrite (Z_to_nat_correct H). stepl ([--](nring (Z_to_nat H)):IR); [| now apply eq_symmetric; apply zring_inv_nat]. apply inv_resp_leEq. apply nring_nonneg. apply less_imp_ap. eapply less_leEq_trans. apply Hx1. rstepl (Pi[/]TwoNZ[+][0]). apply plus_resp_leEq_lft. apply mult_resp_nonneg;[|apply less_leEq; auto with *]. rewrite (Z_to_nat_correct l). stepr (nring (Z_to_nat l):IR); [| now auto with *]. apply nring_nonneg. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac