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