proposition: Lemma BQopp_div_r x y: ratp x -> ratp y -> BQopp (x /q y) = x /q (BQopp y).
proof: Proof. by move => xq yq; rewrite /BQdiv (BQinv_opp yq) BQopp_prod_r //; apply:QS_inv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)