proposition: Lemma BQprodBr x y z: ratp x -> ratp y -> ratp z -> x *q (y -q z) = (x *q y) -q (x *q z).
proof: Proof. move => xq yq qgt0x; rewrite /BQdiff (BQprodDr xq yq (QSo qgt0x)). by rewrite BQopp_prod_r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)