proposition: Lemma AQsin_poly_fun_bound_correct : forall q : AQ, msp_eq (' AQsin_poly_fun (ucFun (AQboundAbs_uc 1) q)) (sin_poly_fun (Qmax (- (1)) (Qmin 1 (' q)))).
proof: Proof. intro q. apply Qball_0. rewrite AQsin_poly_fun_correct. f_equiv. unfold AQboundAbs_uc. simpl. change ('1) with (1:AQ). rewrite ?aq_preserves_max, ?aq_preserves_min. now rewrite ?rings.preserves_negate, ?rings.preserves_1. 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