proposition: Lemma BZ_of_Z_abs x: BZ_of_Z (`|x|) = BZabs (BZ_of_Z x).
proof: Proof. case: x; simpl => p. by rewrite BZabs_pos //; apply:(positive_non_zero1 p). move: (@succ_nz (nat_to_B p)) => snz. by rewrite /BZm_of_nat /BZabs; Ytac0;aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)