proposition: Lemma cos_poly_fun_correct : forall (q:Q), inj_Q IR (cos_poly_fun q)[=][1][-]Two[*](inj_Q IR q[^]2).
proof: Proof. intros q. unfold cos_poly_fun. stepr (inj_Q IR ([1][-]Two*q^2)). apply inj_Q_wd. unfold cg_minus; simpl; ring. stepr (inj_Q IR ([1])[-]inj_Q IR (Two[*]q ^ 2))%Q. apply inj_Q_minus. apply cg_minus_wd. rstepr (nring 1:IR). apply (inj_Q_nring IR 1). stepr (inj_Q IR Two[*]inj_Q IR (q^2)). apply inj_Q_mult. apply mult_wd. apply (inj_Q_nring IR 2). apply (inj_Q_power IR q 2). Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRArith CoRN.reals.fast.CRsin CoRN.reals.fast.CRpi CoRN.reals.fast.CRIR CoRN.reals.fast.Compress Coq.QArith.Qpower CoRN.model.ordfields.Qordfield Coq.QArith.Qround CoRN.transc.Pi CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.ContinuousCorrect CoRN.model.metric2.Qmetric CoRN.transc.SinCos CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra