proposition: Lemma AQarctan_correct (a : AQ) : 'AQarctan a = rational_arctan ('a).
proof: Proof. unfold AQarctan. case (decide_rel _); intros. apply AQarctan_pos_correct. rewrite rings.preserves_negate. rewrite AQarctan_pos_correct. rewrite rings.preserves_negate. apply rational_arctan_opp. Qed.
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