proposition: Lemma cos_eq_0_2PI_1 (x:R) : 0 <= x -> x <= 2 * PI -> x = PI / 2 \/ x = 3 * (PI / 2) -> cos x = 0.
proof: Proof. intros Lo Hi [ -> | -> ]. - now rewrite cos_PI2. - now rewrite cos_3PI2. 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