proposition: Lemma cos_neg : forall x:R, cos (- x) = cos x.
proof: Proof. intro; symmetry in |- *; apply cos_sym. 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