proposition: Lemma BZprod_Mpp b c: inc b BZp -> inc c BZps -> b <=z (b *z c).
proof: Proof. move => pa pb; move:(BZp_sBZ pa) => bb. by move: (BZprod_Mlege0 pa (BZ1_small pb)); rewrite (BZprodC c) BZprod_1l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)