proposition: Lemma ARsin_poly_iter_wd : forall n x y, x = y -> ARsin_poly_iter n x = ARsin_poly_iter n y.
proof: Proof. induction n. - intros. exact H5. - intros. change (ucFun ARsin_poly (ARsin_poly_iter n x) = ucFun ARsin_poly (ARsin_poly_iter n y)). rewrite (IHn x y H5). reflexivity. 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