proposition: Lemma BQdiv_diag_rw: x /q y = \1q -> x = y.
proof: Proof. move => h. case: (equal_or_not y \0q) => h'. by move: h; rewrite h' (BQdiv_x0 xq) => hh; case BQ1_nz. move:(f_equal (BQprod y) h); rewrite (BQprod_div yq xq h'). by rewrite BQprod_1r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)