proposition: Lemma cos_2PI : cos (2 * PI) = 1.
proof: Proof. rewrite cos_2a; rewrite sin_PI; rewrite cos_PI; ring. 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