proposition: Lemma BQprod_Mpp b c: inc b BQp -> \1q <=q c -> b <=q (b *q c).
proof: Proof. move => pa pb. by rewrite BQprodC - {1} (BQprod_1l (BQp_sBQ pa)); apply: BQprod_Mlege0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)