proposition: Lemma cos_correct : forall x, (IRasCR (Cos x) == cos (IRasCR x))%CR.
proof: Proof. intros x. unfold cos. generalize (Qceiling (approximate (IRasCR x * CRinv_pos (6 # 1) (scale 2 CRpi)) (Qpos2QposInf (1 # 2)) - (1 # 2)))%CR. intros z. rewrite -> compress_correct. rewrite <- CRpi_correct, <- CRmult_scale, <- IR_inj_Q_as_CR, <- IR_mult_as_CR, <- IR_minus_as_CR, <- cos_slow_correct. apply IRasCR_wd. rewrite -> inj_Q_mult. change (2:Q) with (Two:Q). rewrite -> inj_Q_nring. rstepr (Cos (x[+]([--](inj_Q IR z))[*](Two[*]Pi))). setoid_replace (inj_Q IR z) with (zring z:IR). rewrite <- zring_inv. symmetry; apply Cos_periodic_Z. rewrite <- inj_Q_zring. apply inj_Q_wd. symmetry; apply zring_Q. 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