proposition: Lemma BQprod_Mltgt0 a b c: inc c BQps -> a <q b -> (a *q c) <q (b *q c).
proof: Proof. move => cp ab; move: (ab) => [[az bz _]_]; move: (BQps_sBQ cp) => cz. move /(qlt_diffP az bz): ab => p1. apply/(qlt_diffP (QSp az cz) (QSp bz cz)). by rewrite - BQprodBl //;apply:QpsS_prod. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)