proposition: Lemma AQcos_poly_uc_correct : forall q : AQ, msp_eq (' AQcos_poly_fun (AQboundAbs_uc 1 q)) (cos_poly_fun (QMinMax.Qmax (- (1)) (QMinMax.Qmin 1 (' q)))).
proof: Proof. intro q. apply Qball_0. rewrite AQcos_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: 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