proposition: Lemma cos_slow_correct : forall x, (IRasCR (Cos x) == cos_slow (IRasCR x))%CR.
proof: Proof. intros x. apply: (ContinuousCorrect (I:proper realline)); [apply Continuous_Cos | | constructor]. intros q [] _. transitivity (rational_cos q);[|apply rational_cos_correct]. unfold cos_slow. pose proof (Cbind_correct QPrelengthSpace cos_uc). apply ucEq_equiv in H. rewrite -> (H (' q))%CR. apply BindLaw1. 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