proposition: Lemma QmpsS_div a b: inc a BQms -> inc b BQps -> inc (a /q b) BQms.
proof: Proof. move => ap bp; rewrite /BQdiv BQprodC. apply:QpmsS_prod => //; apply: (QpsS_inv bp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)