proposition: Lemma ZpS_prod a b: inc a BZp -> inc b BZp -> inc (a *z b) BZp.
proof: Proof. move => az bz; rewrite (BZprod_pp az bz). exact: (BZ_of_natp_i (NS_prod (BZ_valN (BZp_sBZ az))(BZ_valN (BZp_sBZ bz)))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)