proposition: Lemma rational_cos_correct : forall (a:Q), (rational_cos a == IRasCR (Cos (inj_Q IR a)))%CR.
proof: Proof. intros a. unfold rational_cos. rewrite -> rational_sin_correct. apply rational_cos_correct_aux. 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