proposition: Lemma AQsin_bound_correct : forall (a:AQ), -(1 * 3 ^ AQsin_bound a) ≤ a ≤ 1 * 3 ^ AQsin_bound a.
proof: Proof. intro a. unfold AQsin_bound. pose proof (CRsin.sin_bound_correct ('a)). split; apply (order_reflecting (cast AQ Q)). - rewrite rings.preserves_negate. destruct H4, aq_ring, ring_monoid. destruct commonoid_mon. rewrite monoid_left_id. rewrite preserves_nat_pow. rewrite rings.preserves_3. rewrite <-(int_pow_nat_pow (f:=cast nat Z)). rewrite <- (Zpower_Qpower 3). apply H5. apply (Nat2Z.inj_le 0), Nat.le_0_l. - destruct H4, aq_ring, ring_monoid. destruct commonoid_mon. rewrite monoid_left_id. rewrite preserves_nat_pow. rewrite rings.preserves_3. rewrite <-(int_pow_nat_pow (f:=cast nat Z)). rewrite <- (Zpower_Qpower 3). apply H5. apply (Nat2Z.inj_le 0), Nat.le_0_l. 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