proposition: Lemma AQball_bool_true (k : Z) (x y : AQ_as_MetricSpace) : AQball_bool k x y ≡ true ↔ ball (2 ^ k) x y.
proof: Proof. rewrite AQball_abs. unfold AQball_bool. rewrite bool_decide_rel_true. transitivity ('abs (x - y) ≤ ('(1 ≪ k) : Q)). split; intros. now apply (order_preserving _). now apply (order_reflecting (cast AQ Q)). now rewrite aq_shift_correct, rings.preserves_1, left_identity. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program Coq.setoid_ring.Ring CoRN.util.Qdlog CoRN.model.totalorder.QposMinMax CoRN.metric2.Complete CoRN.metric2.Prelength CoRN.model.metric2.Qmetric CoRN.model.metric2.CRmetric CoRN.metric2.MetricMorphisms CoRN.reals.faster.ApproximateRationals