proposition: Lemma zle_abs n: intp n -> n <=z (BZabs n).
proof: Proof. move => nz;case /BZ_i0P: (nz). move => nn; exact (proj1 (zle_pr2 (BZabs_iN nz) nn)). by move => np; rewrite (BZabs_pos np); apply:zleR. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)