proposition: Lemma ARcompress_correct (x : AR) : ARcompress x = x.
proof: Proof. apply regFunEq_equiv, regFunEq_e. intros ε. assert (QposEq (ε + ε) ((1#2) * ε + ((1#2) * ε + ε))) by (unfold QposEq; simpl; ring). apply (ball_wd _ H5 _ _ (reflexivity _) _ _ (reflexivity _)). clear H5. eapply ball_triangle. apply_simplified (aq_approx_dlog2 (approximate x ((1 # 2) * ε)%Qpos) ((1#2) * ε)%Qpos). apply regFun_prf. 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