proposition: Lemma sin_eq_0_0 (x:R) : sin x = 0 -> exists k : Z, x = IZR k * PI.
proof: Proof. intros Hx. destruct (euclidian_division x PI PI_neq0) as (q & r & EQ & Hr & Hr'). exists q. rewrite <- (Rplus_0_r (_*_)). subst. apply Rplus_eq_compat_l. rewrite sin_plus in Hx. assert (H : sin (IZR q * PI) = 0) by (apply sin_eq_0_1; now exists q). rewrite H, Rmult_0_l, Rplus_0_l in Hx. destruct (Rmult_integral _ _ Hx) as [H'|H']. - exfalso. generalize (sin2_cos2 (IZR q * PI)). rewrite H, H', Rsqr_0, Rplus_0_l. intros; now apply R1_neq_R0. - rewrite Rabs_right in Hr'; [|left; apply PI_RGT_0]. destruct Hr as [Hr | ->]; trivial. exfalso. generalize (sin_gt_0 r Hr Hr'). rewrite H'. apply Rlt_irrefl. 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