proposition: Lemma BQdiv_opp_opp x y: ratp x -> ratp y -> (BQopp x) /q (BQopp y) = x /q y.
proof: Proof. move => xq yq. by rewrite -(BQopp_div_l xq (QSo yq)) -BQopp_div_r // BQopp_K //; apply: QS_div. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)