proposition: Lemma cos_eq_0_0 (x:R) : cos x = 0 -> exists k : Z, x = IZR k * PI + PI / 2.
proof: Proof. rewrite cos_sin. intros Hx. destruct (sin_eq_0_0 (PI/2 + x) Hx) as (k,Hk). clear Hx. exists (k-1)%Z. rewrite <- Z_R_minus; simpl. symmetry in Hk. field_simplify [Hk]. field. 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