proposition: Lemma BQprod_opp_opp x y: ratp x -> ratp y -> (BQopp x) *q (BQopp y) = x *q y.
proof: Proof. by move => xq yp; rewrite (BQprod_opp_comm (QSo xq) yp) BQopp_K. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)