proposition: Lemma ZpmS_prod a b: inc a BZp -> inc b BZm -> inc (a *z b) BZm.
proof: Proof. move => az; case /setU1_P; last by move ->; rewrite BZprod_0r;apply: ZmS0. move => bz; case: (equal_or_not a \0z). by move => ->; rewrite BZprod_0l;apply: ZmS0. move => anz; move /BZps_iP: (conj az anz) => sap. by apply /setU1_P; left; apply: ZpmsS_prod. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)