proposition: Lemma ZpmsS_prod a b: inc a BZps -> inc b BZms -> inc (a *z b) BZms.
proof: Proof. move => az bz; move: (BZps_valnz az) (proj1 (BZms_hi_pr bz)) => anz bnz. move: (BZ_valN (BZps_sBZ az)) (BZ_valN (BZms_sBZ bz)) => pa pb. move /BZps_iP: az =>[ap _]; rewrite (BZprod_pm ap bz); apply: BZm_of_natms_i. by apply:NS_prod. by apply cprod2_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)