proposition: Lemma zge0xP x: x <=z \0z <-> inc x BZm.
proof: Proof. split. move => h; apply /setU1_P;case: (equal_or_not x \0z) => xnz; first by right. by left; apply /zgt0xP; split. case /setU1_P; first by case /zgt0xP. move => ->;move: ZS0 => h; BZo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)