proposition: Lemma BZsign_abs x: intp x -> x *z (BZsign x) = BZabs x.
proof: Proof. move => xz; move: (ZS_sign x) => xsp. case /BZ_i1P: (xz) => xs; first by rewrite xs BZprod_0l BZabs_0. by rewrite (BZsign_pos xs) (BZabs_pos (BZps_sBZp xs)) BZprod_1r. by rewrite (BZsign_neg xs) (BZabs_neg xs) (BZprod_m1r xz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)