proposition: Lemma Sin_ap_Zero : forall x:IR, (forall z, x[#](zring z)[*]Pi) -> Sin x [#] [0].
proof: Proof. cut (forall x : IR, [0][<]x -> (forall n : nat, x[#]nring (R:=IR) n[*]Pi) -> Sin x[#][0]). intros X x Hx. destruct (ap_imp_less _ _ _ (Hx 0)). rstepl ([--][--](Sin x)). rstepr ([--][0]:IR). apply inv_resp_ap. csetoid_rewrite_rev (Sin_inv x). apply X. rstepl ([--]([0][*]Pi):IR). apply inv_resp_less. assumption. intros n. csetoid_rewrite_rev (zring_plus_nat IR n). replace (n:Z) with (- - n)%Z by ring. csetoid_rewrite (zring_inv IR (- n)%Z). rstepr ([--](zring (-n)[*]Pi)). apply inv_resp_ap. apply Hx. apply X. rstepl ([0][*]Pi). assumption. intros n. csetoid_rewrite_rev (zring_plus_nat IR n). apply Hx. cut (forall x : IR, [0][<]x -> x[<]Two[*]Pi -> (x[#]Pi) -> Sin x[#][0]). intros X x Hx0 Hx1. assert (Hpi : ([0][<]Two[*]Pi)). apply mult_resp_pos. apply (nring_pos); auto with *. auto with *. destruct (Archimedes' (x[/](Two[*]Pi)[//](Greater_imp_ap _ _ _ Hpi))) as [n Hn]. generalize x Hx0 Hx1 Hn. clear x Hx0 Hx1 Hn. induction n; intros x Hx0 Hx1 Hn. elim (less_antisymmetric_unfolded _ _ _ Hn). apply div_resp_pos; assumption. destruct (ap_imp_less _ _ _ (Hx1 (2*n))). apply IHn; try assumption. apply shift_div_less'. assumption. rstepr ((nring 2[*]nring n)[*]Pi). stepr (nring (R:=IR) (2 * n)[*]Pi). assumption. apply mult_wdl. apply nring_comm_mult. destruct n as [|n]. apply X; try assumption. rstepr ((Two[*]Pi)[*][1]). eapply shift_less_mult'. assumption. rstepr (nring 1:IR). apply Hn. rstepr ((nring 1:IR)[*]Pi). apply Hx1. rstepl (Sin (x[-]Two[*]Pi[+]Two[*]Pi)). csetoid_rewrite (Sin_periodic (x[-]Two[*]Pi)). apply IHn. apply shift_zero_less_minus. eapply leEq_less_trans;[|apply c]. stepr ((Two:IR)[*]nring (S n)[*]Pi); [|csetoid_rewrite (nring_comm_mult IR (2%nat) (S n)); apply eq_reflexive]. rstepl (Two[*]Pi[*]nring 1). rstepr (Two[*]Pi[*]nring (S n)). apply mult_resp_leEq_lft. apply nring_leEq; auto with *. apply less_leEq; assumption. intros i. apply zero_minus_apart. rstepl (x[-]((nring 2[+]nring i)[*]Pi)). apply minus_ap_zero. csetoid_rewrite_rev (nring_comm_plus IR 2 i). apply Hx1. rstepl ((x[/](Two[*]Pi)[//]Greater_imp_ap IR (Two[*]Pi) [0] Hpi)[-](nring 1)). apply shift_minus_less. csetoid_rewrite_rev (nring_comm_plus IR (S n) 1). rewrite Nat.add_comm. assumption. intros x Hx0 Hx1 Hx2. destruct (ap_imp_less _ _ _ Hx2). apply Greater_imp_ap. apply Sin_pos; assumption. rstepl (Sin (x[-]Pi[+]Pi)). csetoid_rewrite (Sin_plus_Pi (x[-]Pi)). rstepr ([--][0]:IR). apply inv_resp_ap. apply Greater_imp_ap. apply Sin_pos. apply shift_zero_less_minus. assumption. apply shift_minus_less. rstepr (Two[*]Pi). assumption. Qed.
imports: CoRN.transc.Pi CoRN.tactics.CornTac