proposition: Lemma ARtoCR_preserves_cos x : 'ARcos x = cos_slow ('x).
proof: Proof. apply preserves_unary_complete_fun. 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