fact: Definition AQarctan_big_pos {a : AQ} (Pa : 1 < a) : msp_car AR := AQpi (1 ≪ (-1)) - AQarctan_small (AQarctan_big_prf a Pa) (AQarctan_big_pos_prf a Pa).
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