proposition: Lemma AQarctan_small_correct : 'AQarctan_small = rational_arctan_small (widen_interval AQarctan_small_Qprf).
proof: Proof. unfold AQarctan_small, rational_arctan_small. rewrite ARtoCR_preserves_plus. apply ucFun2_wd. pose proof CRAR_id. unfold cast. unfold cast in H5. rewrite H5. reflexivity. apply AltSeries_correct. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.nat_pow MathClasses.theory.int_pow CoRN.algebra.RSetoid CoRN.stdlib_omissions.Q CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRarctan_small CoRN.reals.fast.CRarctan CoRN.reals.fast.CRstreams CoRN.reals.fast.CRAlternatingSum CoRN.reals.faster.ARAlternatingSum CoRN.reals.faster.ARsin CoRN.reals.faster.ARArith