proposition: Lemma sin_eq_O_2PI_0 (x:R) : 0 <= x -> x <= 2 * PI -> sin x = 0 -> x = 0 \/ x = PI \/ x = 2 * PI.
proof: Proof. intros Lo Hi Hx. destruct (sin_eq_0_0 x Hx) as (k,Hk). clear Hx. destruct (Rtotal_order PI x) as [Hx|[Hx|Hx]]. - right; right. clear Lo. subst. f_equal. change 2 with (IZR (- (-2))). f_equal. apply Z.add_move_0_l. apply one_IZR_lt1. rewrite plus_IZR; simpl. split. + replace (-1) with (-2 + 1) by ring. apply Rplus_lt_compat_l. apply Rmult_lt_reg_r with PI; [apply PI_RGT_0|]. now rewrite Rmult_1_l. + apply Rle_lt_trans with 0; [|apply Rlt_0_1]. replace 0 with (-2 + 2) by ring. apply Rplus_le_compat_l. apply Rmult_le_reg_r with PI; [apply PI_RGT_0|]. trivial. - right; left; auto. - left. clear Hi. subst. replace 0 with (IZR 0 * PI) by apply Rmult_0_l. f_equal. f_equal. apply one_IZR_lt1. split. + apply Rlt_le_trans with 0; [rewrite <- Ropp_0; apply Ropp_gt_lt_contravar, Rlt_0_1 | ]. apply Rmult_le_reg_r with PI; [apply PI_RGT_0|]. now rewrite Rmult_0_l. + apply Rmult_lt_reg_r with PI; [apply PI_RGT_0|]. now rewrite Rmult_1_l. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Rtrigo_def Rtrigo_alt Cos_rel Cos_plus ZArith_base Zcomplements Lia Lra Ranalysis1 Rsqrt_def PSeries_reg