proposition: Lemma zgt0xP x: x <z \0z <-> inc x BZms.
proof: Proof. split. move => pa; case /BZ_i0P: (proj31_1 pa) => //. move /zle0xP => h; BZo_tac. move => h; move: (zleT_el ZS0 (BZms_sBZ h)); case => //. move /zle0xP => h1;case:(BZ_di_neg_pos h h1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)