proposition: Lemma BQopp_prod_r x y: ratp x -> ratp y -> BQopp (x *q y) = x *q (BQopp y).
proof: Proof. move => xq yq. by rewrite - (BQprod_m1r (QSp xq yq)) - (BQprodA xq yq QSm1) (BQprod_m1r yq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)