proposition: Lemma QpS_prod a b: inc a BQp -> inc b BQp -> inc (a *q b) BQp.
proof: Proof. move: QpS0 => h ap bp; move:(BQp_sBQ ap)(BQp_sBQ bp) => aq bq. case: (equal_or_not a \0q) => e1; first by rewrite e1 BQprod_0l. case: (equal_or_not b \0q) => e2; first by rewrite e2 BQprod_0r. by apply:(BQps_sBQp); apply:QpsS_prod; apply/BQps_iP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)