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