proposition: Lemma ARmult_bounded_mult (x y : AR) c : -'c ≤ y ≤ 'c → ARmult_bounded c x y = x * y.
proof: Proof. intros. apply (injective (cast AR CR)). rewrite ARtoCR_preserves_mult, ARtoCR_preserves_mult_bounded. destruct c as [c Pc]. apply CRmult_bounded_mult. change (cast Q CR (-cast AQ Q c) ≤ cast AR CR y). rewrite <-rings.preserves_negate. rewrite <-ARtoCR_inject. apply (order_preserving _). intuition. change (cast AR CR y ≤ cast Q CR (cast AQ Q c)). rewrite <-ARtoCR_inject. apply (order_preserving _). intuition. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program Coq.setoid_ring.Ring Coq.QArith.Qabs CoRN.stdlib_omissions.Q MathClasses.misc.workaround_tactics CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.util.Qdlog CoRN.metric2.Complete CoRN.metric2.Prelength CoRN.model.metric2.Qmetric CoRN.metric2.MetricMorphisms CoRN.reals.fast.CRArith CoRN.reals.fast.CRpower MathClasses.implementations.stdlib_binary_naturals MathClasses.orders.minmax MathClasses.implementations.positive_semiring_elements CoRN.reals.faster.ApproximateRationals CoRN.reals.faster.AQmetric