fact: Definition AQarctan (a : AQ) : msp_car AR := match decide_rel (≤) 0 a with | left Pa => AQarctan_pos Pa | right Pa => -AQarctan_pos (AQarctan_prf Pa) end.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.metric2.MetricMorphisms CoRN.reals.fast.CRarctan_small CoRN.reals.fast.CRarctan CoRN.reals.fast.CRpi_fast CoRN.reals.faster.ARpi CoRN.reals.faster.ARarctan_small CoRN.reals.faster.ARArith