proposition: Lemma BQprod_CA x y z: ratp x -> ratp y -> ratp z -> x *q (y *q z) = y *q (x *q z).
proof: Proof. by move => xz yz zz;rewrite (BQprodA xz yz zz) (BQprodA yz xz zz) (BQprodC x y). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)