proposition: Lemma Qball_Qdiv_inv (d z: Qpos) (x y: Q): Qball (proj1_sig d / proj1_sig z) (x / proj1_sig z) (y / proj1_sig z) -> Qball (proj1_sig d) x y.
proof: Proof. intros. rewrite <- (Qmult_1_r x), <- (Qmult_1_r y), <- (Qmult_inv_r (proj1_sig z)), (Qmult_comm (proj1_sig z)), Qmult_assoc, Qmult_assoc... apply Qball_Qmult_r... auto. intro abs. destruct z. simpl in abs. clear H. rewrite abs in q. exact (Qlt_irrefl _ 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