proposition: Lemma BZprod_Mlele0 a b c: inc c BZm -> a <=z b -> (b *z c) <=z (a *z c).
proof: Proof. move => cm; move: (BZopp_negative2 cm) => ocp ineq. move: (BZprod_Mlege0 ocp (zle_opp ineq)). move: ineq => [az bz _]; move: (BZm_sBZ cm) => cz. rewrite BZprod_opp_opp // BZprod_opp_opp //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)