proposition: Lemma BQdiv_div2 a b c: ratp a -> ratp b -> ratp c -> a /q (b *q c) = (a /q b) /q c.
proof: Proof. move => aq bq cq. by rewrite /BQdiv (BQprod_inv bq cq) BQprodA //; apply: QS_inv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)