proposition: Lemma COS_bound : forall x:R, -1 <= cos x <= 1.
proof: Proof. intro; rewrite <- sin_shift; apply SIN_bound. 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