proposition: Lemma BQdiv_div_simp a b c: ratp a -> ratp b -> ratp c -> b <> \0q -> (a /q b) /q (c /q b) = a /q c.
proof: Proof. move => aq bq cq bnz. move: (QS_inv bq) (QS_inv cq) => biq ciq. rewrite /BQdiv (BQinv_div cq bq) (BQprodC a). rewrite (BQprod_ACA biq aq bq ciq) (BQprodC _ b) BQprod_inv1 //. by rewrite BQprod_1l //; apply:QSp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)