proposition: Lemma sin_2a : forall x:R, sin (2 * x) = 2 * sin x * cos x.
proof: Proof. intro x; rewrite <-Rplus_diag; rewrite sin_plus. rewrite <- (Rmult_comm (sin x)); symmetry in |- *; rewrite Rmult_assoc; symmetry; apply Rplus_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