proposition: Lemma BQdiv_abs x y: ratp x -> ratp y -> (BQabs x) /q (BQabs y) = BQabs (x /q y).
proof: Proof. move => xq yq. by rewrite /BQdiv (BQprod_abs xq (QS_inv yq)) (BQinv_abs yq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)