proposition: Lemma gball_Qabs (e a b : Q) : ball e a b <-> (Qabs (a - b) <= e).
proof: Proof. simpl. unfold Qball. rewrite <- AbsSmall_Qabs. reflexivity. 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