proposition: Lemma sin_eq_0_1 : forall x:R, (exists k : Z, x = IZR k * PI) -> sin x = 0.
proof: Proof. assert (forall n, sin (INR n * PI) = 0). { intros n;induction n as [|n IHn]. { change (INR 0) with 0. replace (0 * PI) with 0 by ring. exact sin_0. } rewrite S_INR. replace ((INR n + 1) * PI) with ((INR n) * PI + PI) by ring. rewrite neg_sin,IHn. ring. } intros x [k Hx]. rewrite Hx;clear x Hx. destruct (Z.abs_or_opp_abs k). - replace (IZR k) with (INR (Z.to_nat k)). { apply H. } rewrite INR_IZR_INZ. f_equal. apply Z2Nat.id. lia. - replace (IZR k) with (- INR (Z.to_nat (- k))). { replace (- INR (Z.to_nat (- k)) * PI) with (- (INR (Z.to_nat (- k)) * PI)) by ring. rewrite sin_neg. rewrite H;ring. } rewrite INR_IZR_INZ. rewrite <-opp_IZR. f_equal. lia. 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