proposition: Lemma QmsuS_prod a b: inc a BQms -> inc b BQms -> inc (a *q b) BQps.
proof: Proof. move => aq bq. move: (QpsS_prod (BQopp_negative1 aq) (BQopp_negative1 bq)). by rewrite BQprod_opp_opp //; apply:BQms_sBQ. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)