proposition: Lemma QmuS_div a b: inc a BQm -> inc b BQm -> inc (a /q b) BQp.
proof: Proof. move: QpS0 => izp ap bp; move:(BQm_sBQ ap)(BQm_sBQ bp)=> aq bq. case: (equal_or_not a \0q) => az; first by rewrite az BQdiv_0x. case: (equal_or_not b \0q) => bz; first by rewrite bz BQdiv_x0. by apply/(BQps_sBQp); apply:QmsuS_div; apply/BQms_iP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)