proposition: Lemma sin_minus : forall x y:R, sin (x - y) = sin x * cos y - cos x * sin y.
proof: Proof. intros; unfold Rminus in |- *; rewrite sin_plus. rewrite <- cos_sym; rewrite sin_antisym; 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