proposition: Lemma BQprod_Mpp1 a b: \1q <=q a -> \1q <=q b -> \1q <=q a *q b.
proof: Proof. move => a1 b1. have [h _]: \0q <q \1q by move / qlt0xP:QpsS1. have ap: inc a BQp by apply / qle0xP; BQo_tac. exact:(qleT a1 (BQprod_Mpp ap b1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)