proposition: Lemma Qball_Qmult_Q_r : Qball (proj1_sig d) (x * z) (y * z).
proof: Proof. destruct (Qeq_dec z 0) as [E|E]. rewrite E, Qmult_0_r, Qmult_0_r. apply Qball_Reflexive. apply Qpos_nonneg. apply Qball_Qabs. apply Qball_Qabs in B. assert (Qeq (x * z - y * z) ((x - y) * z)) by (simpl; ring). rewrite H. clear H. rewrite Qabs_Qmult. assert (0 < Qabs z). { apply Qabs_case. intros. apply Qle_lteq in H. destruct H. exact H. contradict E. symmetry. exact H. intros. apply Qle_lteq in H. destruct H. apply (Qplus_lt_l _ _ z). ring_simplify. exact H. contradict E. exact H. } simpl in B. apply (Qmult_le_l _ _ (/(Qabs z))). apply Qinv_lt_0_compat, H. rewrite Qmult_comm, <- Qmult_assoc, Qmult_inv_r, Qmult_1_r. rewrite Qmult_comm. exact B. intro abs. rewrite abs in H. exact (Qlt_irrefl _ 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