proposition: Lemma ZmsuS_prod a b: inc a BZms -> inc b BZms -> inc (a *z b) BZps.
proof: Proof. move => az bz;apply/BZps_iP ; split. rewrite (BZprod_mm az bz); apply :BZ_of_natp_i. by apply:NS_prod;apply:BZ_valN; apply: BZms_sBZ. move/BZms_iP: az => [/BZm_sBZ az a0]. move/BZms_iP: bz => [/BZm_sBZ bz b0]. by apply:BZprod_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)