proposition: Lemma cos_2a : forall x:R, cos (2 * x) = cos x * cos x - sin x * sin x.
proof: Proof. intro x; rewrite <-Rplus_diag; apply cos_plus. 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