proposition: Lemma BZms_iP x: inc x BZms <-> (inc x BZm /\ x <> \0z).
proof: Proof. split; last by move => [] /setU1_P; case. by move => h; move: (BZms_nz h)=> xnz;split => //; apply /setU1_P;left. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)