proposition: Lemma BZprod_Mltgt0 a b c: inc c BZps -> a <z b -> (a *z c) <z (b *z c).
proof: Proof. move => cp ab; move: (ab) => [[az bz _]_]; move: (BZps_sBZ cp) => cz. move /(zlt_diffP az bz): ab => p1. apply/(zlt_diffP (ZSp az cz) (ZSp bz cz)). by rewrite - BZprodBl //;apply:ZpsS_prod. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)