proposition: Lemma ARtoCR_preserves_AQpi x : 'AQpi x = r_pi ('x).
proof: Proof. unfold AQpi, r_pi. assert (∀ (k : Z) (d : positive) (Pnd: -(cast Z AQ (Zpos d)) < 1 < cast Z AQ (Zpos d)) (dpos : 0 < cast Z AQ (Zpos d)) (Pa : (-1 <= 1#d <= 1)%Q), ' ucFun (ARscale ('k * x)) (AQarctan_small Pnd dpos) = ucFun (scale (inject_Z k * 'x)) (rational_arctan_small Pa)) as PP. { intros. rewrite ARtoCR_preserves_scale. apply Cmap_wd. rewrite rings.preserves_mult, AQtoQ_ZtoAQ. reflexivity. rewrite AQarctan_small_correct. rewrite rational_arctan_small_wd. reflexivity. rewrite rings.preserves_1. pose proof (AQtoQ_ZtoAQ (Zpos d)). rewrite H5. reflexivity. } assert (forall x y : msp_car AR, ARtoCR (x+y) = 'x + 'y) as plusMorph. { intros x0 y. apply (rings.preserves_plus x0 y). } unfold cast. unfold cast in plusMorph. rewrite plusMorph. apply ucFun2_wd. rewrite plusMorph. apply ucFun2_wd. apply PP. apply PP. rewrite plusMorph. apply ucFun2_wd. apply PP. apply PP. Qed.
imports: MathClasses.interfaces.abstract_algebra CoRN.stdlib_omissions.Q CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRpi_fast CoRN.reals.fast.CRarctan_small CoRN.reals.faster.ARarctan_small