proposition: Lemma cos_2a_sin : forall x:R, cos (2 * x) = 1 - 2 * sin x * sin x.
proof: Proof. intro x; rewrite Rmult_assoc; unfold Rminus in |- *; repeat rewrite <-Rplus_diag. generalize (sin2_cos2 x); intro H1; rewrite <- H1; rewrite cos_plus; ring_Rsqr. 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