proposition: Lemma form3 : forall p q:R, sin p + sin q = 2 * cos ((p - q) / 2) * sin ((p + q) / 2).
proof: Proof. intros p q; pattern p at 1 in |- *; replace p with ((p - q) / 2 + (p + q) / 2). - pattern q at 3 in |- *; replace q with ((p + q) / 2 - (p - q) / 2). + rewrite sin_plus; rewrite sin_minus; ring. + pattern q at 3 in |- *; rewrite <-Rplus_half_diag; unfold Rdiv in |- *; ring. - pattern p at 3 in |- *; rewrite <-Rplus_half_diag; unfold Rdiv in |- *; 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