proposition: Lemma BZabs_sign x: intp x -> x = (BZsign x) *z (BZabs x).
proof: Proof. move => xz; move: (ZSa xz) => az. case /BZ_i1P: (xz) => xs; first by rewrite xs BZabs_0 BZprod_0r. by rewrite (BZsign_pos xs) (BZabs_pos (BZps_sBZp xs)) BZprod_1l. by rewrite (BZsign_neg xs) (BZabs_neg xs) (BZprod_m1l (ZSo xz)) (BZopp_K xz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)