proposition: Lemma sin_eq_O_2PI_1 (x:R) : 0 <= x -> x <= 2 * PI -> x = 0 \/ x = PI \/ x = 2 * PI -> sin x = 0.
proof: Proof. intros _ _ [ -> |[ -> | -> ]]. - now rewrite sin_0. - now rewrite sin_PI. - now rewrite sin_2PI. 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