proposition: Lemma QpS_div a b: inc a BQp -> inc b BQp -> inc (a /q b) BQp.
proof: Proof. move: QpS0 => izp ap bp; move:(BQp_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/(BQps_sBQp); apply:QpsS_div; apply/BQps_iP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)