proposition: Lemma BQprod_Mlele0 a b c: inc c BQm -> a <=q b -> (b *q c) <=q (a *q c).
proof: Proof. move => cm; move: (BQopp_negative2 cm) => ocp ineq. move: (BQprod_Mlege0 ocp (qle_opp ineq)). move: ineq => [az bz _]; move: (BQm_sBQ cm) => cz. rewrite BQprod_opp_opp // BQprod_opp_opp //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)