proposition: Lemma QpmsS_prod a b: inc a BQps -> inc b BQms -> inc (a *q b) BQms.
proof: Proof. move => aq bq. have h := (BQopp_negative1 bq). rewrite -(BQopp_K (BQms_sBQ bq)). rewrite - (BQopp_prod_r (BQps_sBQ aq) (BQps_sBQ h)). apply: BQopp_positive1; apply:(QpsS_prod aq h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)