proposition: Lemma BQdiv_prod_simpl_r: z <> \0q -> (x *q z) /q (y *q z) = x /q y.
proof: Proof. by move => h; rewrite (BQprodC x z) (BQprodC y z); apply: BQdiv_prod_simpl_l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)