fact: Definition AQpi (x : AQ) : msp_car AR := ucFun (ARscale (' 176%Z * x)) (AQarctan_small (AQpi_prf 57 eq_refl) (ZtoAQ_pos 57 eq_refl)) + ucFun (ARscale (' 28%Z * x)) (AQarctan_small (AQpi_prf 239 eq_refl) (ZtoAQ_pos 239 eq_refl)) + (ucFun (ARscale (' (-48)%Z * x)) (AQarctan_small (AQpi_prf 682 eq_refl) (ZtoAQ_pos 682 eq_refl)) + ucFun (ARscale (' 96%Z * x)) (AQarctan_small (AQpi_prf 12943 eq_refl) (ZtoAQ_pos 12943 eq_refl))).
imports: MathClasses.interfaces.abstract_algebra CoRN.stdlib_omissions.Q CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRpi_fast CoRN.reals.fast.CRarctan_small CoRN.reals.faster.ARarctan_small