proposition: Lemma AQsin_small_Qprf : -1 ≤ AQtoQ num / AQtoQ den ≤ 1.
proof: Proof. split. - apply Qle_shift_div_l. pose proof (rings.preserves_0 (f:=cast AQ Q)). rewrite <- H5. apply (strictly_order_preserving (cast AQ Q)), dpos. setoid_replace (-1 * AQtoQ den) with (-AQtoQ den) by reflexivity. rewrite <- rings.preserves_negate. apply (order_preserving (cast AQ Q)), Pnd. - apply Qle_shift_div_r. pose proof (rings.preserves_0 (f:=cast AQ Q)). rewrite <- H5. apply (strictly_order_preserving (cast AQ Q)), dpos. rewrite Qmult_1_l. apply (order_preserving (cast AQ Q)), Pnd. 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