proposition: Lemma BQmpS_div a b: inc a BQm -> inc b BQp -> inc (a /q b) BQm.
proof: Proof. move: QmS0 => izp ap bp; move:(BQm_sBQ ap)(BQp_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/(BQms_sBQm); apply:QmpsS_div; [ apply/BQms_iP | apply/BQps_iP ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)