proposition: Lemma sin_PI_x : forall x:R, sin (PI - x) = sin x.
proof: Proof. intro x; rewrite sin_minus; rewrite sin_PI; rewrite cos_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