proposition: Lemma ZSp x y: intp x -> intp y -> intp (x *z y).
proof: Proof. move => pa pb. move: (BZ_of_nat_i (NS_prod (BZ_valN pa)(BZ_valN pb))) => h. rewrite BZprodE /BZprod_int;Ytac h1 => //; apply: ZSo => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)