proposition: Lemma ZpsS_prod a b: inc a BZps -> inc b BZps -> inc (a *z b) BZps.
proof: Proof. move => /BZps_iP [ap anz] /BZps_iP [bp bnz]; apply/BZps_iP ; split. by apply: ZpS_prod. by move:(BZp_sBZ ap) (BZp_sBZ bp) => az bz; apply:BZprod_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)