proposition: Lemma BQprod_Mltltgt0 a b c d: inc b BQps -> inc c BQps -> a <q b -> c <q d -> (a *q c) <q (b *q d).
proof: Proof. move => pa pb pc pd. move: (BQprod_Mltgt0 pb pc) (BQprod_Mltgt0 pa pd) => r1. rewrite (BQprodC c) (BQprodC d) => r2; BQo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)