proposition: Lemma BQdiv_prod: x <> \0q -> (x *q y) /q x = y.
proof: Proof. move => h; rewrite /BQdiv BQprodC (BQprodA (QS_inv xq) xq yq). by rewrite (BQprodC _ x) BQprod_inv1 // BQprod_1l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)