proposition: Lemma BZprod_abs x y: intp x -> intp y -> BZabs (x *z y) = (BZabs x) *z (BZabs y).
proof: Proof. move => pa pb. rewrite (BZprod_pp (BZabs_iN pa) (BZabs_iN pb)). by rewrite (BZprod_abs2 pa pb) /BZabs /BZ_of_nat; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)