proposition: Lemma Qball_opp (e : Q) (x x' : Q): Qball e x x' -> Qball e (-x) (-x').
proof: Proof. Proof with auto. intros. apply Qball_Qabs. unfold Qminus. rewrite Qopp_involutive. rewrite Qplus_comm. apply Qball_Qabs. apply ball_sym... 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