proposition: Lemma AQarctan_pos_correct {a : AQ} `(Pa : 0 ≤ a) : 'AQarctan_pos Pa = rational_arctan ('a).
proof: Proof. unfold AQarctan_pos. case (decide_rel _); intros. rewrite AQarctan_small_correct. rewrite rational_arctan_small_correct. rewrite rational_arctan_correct. apply CRIR.IRasCR_wd, InvTrigonom.ArcTan_wd, Q_in_CReals.inj_Q_wd. mc_setoid_replace (('a / '1)%mc : Q) with ('a). reflexivity. rewrite rings.preserves_1. rewrite dec_fields.dec_recip_1. now apply rings.mult_1_r. case (decide_rel _); intros. apply AQarctan_mid_pos_correct. apply AQarctan_big_pos_correct. 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