proposition: Lemma QmuS_prod a b: inc a BQm -> inc b BQm -> inc (a *q b) BQp.
proof: Proof. move => az bz. move: (QpS_prod (BQopp_negative2 az) (BQopp_negative2 bz)). by rewrite BQprod_opp_opp //; apply: BQm_sBQ. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)