proposition: Lemma form2 : forall p q:R, cos p - cos q = -2 * sin ((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) by field. rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2) by field. rewrite cos_plus; rewrite cos_minus; 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