proposition: Lemma AQarctan_mid_pos_correct {a : AQ} `(Pa : 0 < a) : 'AQarctan_mid_pos Pa = rational_arctan ('a).
proof: Proof. unfold AQarctan_mid_pos. rewrite rings.preserves_plus. rewrite ARtoCR_preserves_AQpi. transitivity (r_pi (' (1 ≪ (-2))) + rational_arctan (('a - 1) / ('a + 1) : Q)). apply ucFun2_wd. reflexivity. 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) / '(a + 1) : Q) with (('a - 1) / ('a + 1) : Q). reflexivity. rewrite rings.preserves_minus, rings.preserves_plus. now rewrite rings.preserves_1. rewrite aq_shift_opp_2, rings.preserves_1. apply rational_arctan_fourth_pi. now apply semirings.preserves_pos. 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