proposition: Lemma Qball_ex_bool_correct (ε : Qpos) x y : Is_true (Qball_ex_bool ε x y) <-> Qball (proj1_sig ε) x y.
proof: Proof. split; intros E. apply Is_true_eq_true in E. unfold Qball_ex_bool in E. destruct (ball_ex_dec Q_as_MetricSpace Qmetric_dec ε x y). apply b. discriminate. apply Is_true_eq_left. unfold Qball_ex_bool. destruct (ball_ex_dec Q_as_MetricSpace Qmetric_dec ε x y). reflexivity. contradiction. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.Prelength CoRN.metric2.Classification CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs CoRN.metric2.UniformContinuity MathClasses.implementations.stdlib_rationals Coq.QArith.Qround