proposition: Lemma ARtoCR_preserves_mult x y : cast AR CR (x * y) = 'x * 'y.
proof: Proof. unfold "*", ARmult at 1. rewrite ARtoCR_preserves_mult_bounded. assert (QposEq ('AR_b y : Qpos) (CR_b (1 # 1) ('y))). { unfold QposEq. simpl. now rewrite ARtoCR_approximate, <-AR_b_correct. } apply (CRmult_bounded_wd H5). 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