proposition: Lemma AQarctan_big_pos_correct {a : AQ} `(Pa : 1 < a) : 'AQarctan_big_pos Pa = rational_arctan ('a).
proof: Proof. unfold AQarctan_big_pos. rewrite rings.preserves_minus. rewrite ARtoCR_preserves_AQpi. rewrite aq_shift_opp_1, rings.preserves_1. transitivity (r_pi (1 / 2)%mc - rational_arctan (/ ' a)). apply ucFun2_wd. reflexivity. rewrite AQarctan_small_correct. rewrite rational_arctan_small_correct. rewrite rational_arctan_correct. apply Cmap_wd. reflexivity. apply CRIR.IRasCR_wd, InvTrigonom.ArcTan_wd, Q_in_CReals.inj_Q_wd. now rewrite rings.preserves_1, rings.mult_1_l. apply rational_arctan_half_pi. transitivity (1:Q). now apply (semirings.lt_0_1 (R:=Q)). now apply semirings.preserves_gt_1. 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