proposition: Lemma cos_sin : forall x:R, cos x = sin (PI / 2 + x).
proof: Proof. intro x; rewrite sin_plus; rewrite sin_PI2; rewrite cos_PI2; 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