proposition: Lemma BZprod_Mltlt0 a b c: inc c BZms -> a <z b -> (b *z c) <z (a *z c).
proof: Proof. move => cm; move: (BZopp_negative1 cm) => ocp ineq. move: (BZprod_Mltgt0 ocp (zlt_opp ineq)). move: ineq => [[az bz _] _]; move: (BZms_sBZ cm) => cz. rewrite BZprod_opp_opp // BZprod_opp_opp //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)