proposition: Lemma rational_cos_correct_aux a : (cos_poly (IRasCR (Sin (inj_Q IR (a / 2)))) == IRasCR (Cos (inj_Q IR a)))%CR.
proof: Proof. rewrite <- cos_poly_correct. apply IRasCR_wd. csetoid_rewrite_rev (Cos_double_angle (inj_Q IR (a/2))). apply Cos_wd. csetoid_replace (Two:IR) (inj_Q IR (2:Q));[|apply eq_symmetric; apply (inj_Q_nring IR 2)]. stepl (inj_Q IR (2*(a/2))); [| now apply inj_Q_mult]. apply inj_Q_wd. simpl; field; discriminate. apply AbsIR_imp_AbsSmall. stepr (nring 1:IR); [| now (apply eq_symmetric; apply (inj_Q_nring IR 1))]. rstepr ([1]:IR). apply AbsIR_Sin_leEq_One. 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