proposition: Lemma AQsin_small_pos_wd : forall (n1 n2 d1 d2 : AQ) (p1 : -d1 ≤ n1 ≤ d1) (p2 : -d2 ≤ n2 ≤ d2) (d1pos : 0 < d1) (d2pos : 0 < d2), n1 = n2 -> d1 = d2 -> AQsin_small p1 d1pos = AQsin_small p2 d2pos.
proof: Proof. assert (forall x y, ARtoCR x = ARtoCR y -> x = y) as H5. { intros x y H5. exact H5. } intros. apply H5. rewrite (AQsin_small_correct p1 d1pos). rewrite (AQsin_small_correct p2 d2pos). rewrite H6, H7. reflexivity. 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