proposition: Lemma sin_plus : forall x y:R, sin (x + y) = sin x * cos y + cos x * sin y.
proof: Proof. intros. rewrite (sin_cos (x + y)). replace (PI / 2 + (x + y)) with (PI / 2 + x + y); [ rewrite cos_plus | ring ]. rewrite (sin_cos (PI / 2 + x)). replace (PI / 2 + (PI / 2 + x)) with (x + PI). - rewrite neg_cos. replace (cos (PI / 2 + x)) with (- sin x). + ring. + rewrite sin_cos; rewrite Ropp_involutive; reflexivity. - pattern PI at 1 in |- *; rewrite <-(Rplus_half_diag PI); 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