proposition: Lemma Qball_e_wd : forall (e1 e2:Q) x y, e1 == e2 -> (Qball e1 x y <-> Qball e2 x y).
proof: Proof. intros. unfold Qball, QAbsSmall. rewrite -> H. 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