proposition: Lemma AQsin_poly_fun_correct (q : AQ) : 'AQsin_poly_fun q = sin_poly_fun ('q).
proof: Proof. unfold AQsin_poly_fun, sin_poly_fun. rewrite nat_pow_2. rewrite rings.preserves_mult, rings.preserves_minus, ?rings.preserves_mult. rewrite rings.preserves_3, rings.preserves_4. now rewrite <-(associativity _ ('q) ('q : Q)). Qed.
imports: Coq.QArith.Qround Coq.QArith.Qpower MathClasses.interfaces.abstract_algebra MathClasses.theory.nat_pow MathClasses.theory.int_pow CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.MetricMorphisms CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.util.Qdlog CoRN.stdlib_omissions.Q CoRN.reals.fast.CRsin CoRN.reals.fast.CRstreams CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.Compress CoRN.reals.faster.ARAlternatingSum CoRN.reals.faster.ARArith