proposition: Lemma BQprod_Mltlt0 a b c: inc c BQms -> a <q b -> (b *q c) <q (a *q c).
proof: Proof. move => cm; move: (BQopp_negative1 cm) => ocp ineq. move: (BQprod_Mltgt0 ocp (qlt_opp ineq)). move: ineq => [[az bz _] _]; move: (BQms_sBQ cm) => cz. rewrite BQprod_opp_opp // BQprod_opp_opp //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)