proposition: Lemma BQdiv_prod_simpl_l: x <> \0q -> (x *q y) /q (x *q z) = y /q z.
proof: Proof. move => xnz. rewrite /BQdiv (BQprod_inv xq zq) (BQprodC x y). rewrite (BQprodA (QSp yq xq) (QS_inv xq) (QS_inv zq)). by rewrite -(BQprodA yq xq (QS_inv xq)) BQprod_inv1 // BQprod_1r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)