proposition: Lemma BQprod_AC x y z: ratp x -> ratp y -> ratp z -> (x *q y) *q z = (x *q z) *q y.
proof: Proof. move => xq yq zq. by rewrite - (BQprodA xq yq zq) - (BQprodA xq zq yq) (BQprodC y). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)