proposition: Lemma QAbsSmall_opp : forall x y : Q, QAbsSmall x y -> QAbsSmall x (-y).
proof: Proof. intros x y H. split. apply Qopp_le_compat. apply H. rewrite <- (Qopp_involutive x). apply Qopp_le_compat. apply H. 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