proposition: Lemma AQcos_poly_fun_correct (x : AQ) : 'AQcos_poly_fun x = cos_poly_fun ('x).
proof: Proof. unfold AQcos_poly_fun, cos_poly_fun. rewrite nat_pow.nat_pow_2. rewrite rings.preserves_minus, ?rings.preserves_mult. rewrite rings.preserves_1, rings.preserves_2. now rewrite associativity. 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