proposition: Lemma BZ_i1P x: intp x <-> [\/ x = \0z, inc x BZps | inc x BZms].
proof: Proof. split. move /BZ_i0P; case => h; first by constructor 3. case: (equal_or_not x \0z); first by constructor 1. by constructor 2; apply /BZps_iP. case; [move ->; apply:ZS0 | apply:BZps_sBZ | apply:BZms_sBZ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)