proposition: Lemma cos_PI : cos PI = -1.
proof: Proof. replace PI with (PI / 2 + PI / 2). - rewrite cos_plus. rewrite sin_PI2; rewrite cos_PI2. ring. - apply Rplus_half_diag. 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