fact: Definition AQarctan_pos {a : AQ} (Pa1 : 0 ≤ a) : msp_car AR := match decide_rel (≤) a (1 ≪ (-1)) with | left Pa2 => AQarctan_small (AQarctan_pos_prf1 Pa1 Pa2) semirings.lt_0_1 | right Pa2 => match decide_rel (≤) a 2 with | left Pa3 => AQarctan_mid_pos (AQarctan_pos_prf2 Pa2) | right Pa3 => AQarctan_big_pos (AQarctan_pos_prf3 Pa3) end 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