proposition: Lemma Q_approx_correct (x : Q) (k : Z) : Qball (2 ^ k) (app_approx x k) x.
proof: Proof. destruct k as [|p|]. - apply ball_refl. discriminate. - apply ball_refl. apply Qpower.Qpower_pos_positive. discriminate. - unfold app_approx, Q_approx. setoid_replace (2 ^ Zneg p)%Q with (1 # (2 ^ p))%Q. now apply ball_sym, approximateQ_correct. change (/ Qpower (inject_Z 2%Z) (Zpos p) == 1 # 2 ^ p). rewrite <-Qpower.Zpower_Qpower; auto with zarith. now rewrite <- Zpower_Ppow. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.QArith CoRN.util.Qdlog Coq.ZArith.ZArith CoRN.reals.fast.Compress CoRN.metric2.MetricMorphisms CoRN.model.metric2.Qmetric CoRN.reals.faster.ARArith CoRN.model.totalorder.QposMinMax