proposition: Lemma Qball_Qmult_r: Qball (proj1_sig d) (x * proj1_sig z) (y * proj1_sig z).
proof: Proof. apply Qball_Qmult_Q_r. destruct z, x0, Qnum; simpl. exfalso. apply (Qlt_not_le _ _ q). simpl. apply (Qle_refl 0). exact B. exfalso. inversion q. 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