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