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