proposition: Lemma cos_eq_0_1 (x:R) : (exists k : Z, x = IZR k * PI + PI / 2) -> cos x = 0.
proof: Proof. rewrite cos_sin. intros (k,->). replace (_ + _) with (IZR k * PI + PI) by field. rewrite neg_sin, <- Ropp_0. apply Ropp_eq_compat. apply sin_eq_0_1. now exists k. 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