proposition: Lemma AQcos_correct a : 'AQcos a = rational_cos ('a).
proof: Proof. unfold AQcos. rewrite ARtoCR_preserves_cos_poly. posed_rewrite AQsin_correct. rewrite aq_shift_opp_1. now apply rational_cos_sin. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.metric2.Qmetric MathClasses.misc.workaround_tactics CoRN.reals.fast.CRsin CoRN.reals.fast.CRcos CoRN.metric2.MetricMorphisms CoRN.metric2.Complete CoRN.reals.faster.ARsin MathClasses.interfaces.abstract_algebra CoRN.reals.faster.ARArith