proposition: Lemma zlt0xP x: \0z <z x <-> inc x BZps.
proof: Proof. split. by move => [/zle0xP pa /nesym pb]; apply /BZps_iP. by move /BZps_iP => [pa pb]; split; [apply /zle0xP |apply: nesym]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)