proposition: Lemma zle0xP x: \0z <=z x <-> inc x BZp.
proof: Proof. split. move => [pa pb pc]; case /BZ_i0P: pb => // xn. have h: int_np \0z -> False by rewrite /int_np BZ0_sg; fprops. case: pc; case => // _. by move: (BZms_sg xn); rewrite /int_pp /int_np => -> /C0_ne_C1. move => xp. move:(BZp_sBZ xp) ZS0 => xz z0; split => //; constructor 3. split; [ exact BZ0_sg | exact: (BZp_sg xp) | ]. by move: (BZ_valN (BZp_sBZ xp)) =>/cle0n; rewrite BZ0_val. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)