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