proposition: Lemma AQsin_small_correct : 'AQsin_small = rational_sin (AQtoQ num / AQtoQ den).
proof: Proof. rewrite rational_sin_correct, <- (rational_sin_small_correct AQsin_small_Qprf). unfold AQsin_small, rational_sin_small. rewrite ARtoCR_preserves_plus. apply ucFun2_wd. pose proof CRAR_id. unfold cast in H5. unfold cast. rewrite H5. reflexivity. apply AltSeries_correct. Qed.
imports: Coq.QArith.Qround Coq.QArith.Qpower MathClasses.interfaces.abstract_algebra MathClasses.theory.nat_pow MathClasses.theory.int_pow CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.MetricMorphisms CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.util.Qdlog CoRN.stdlib_omissions.Q CoRN.reals.fast.CRsin CoRN.reals.fast.CRstreams CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.Compress CoRN.reals.faster.ARAlternatingSum CoRN.reals.faster.ARArith