proposition: Lemma BZ_i2P x: intp x <-> (inc x BZps \/ inc x BZm).
proof: Proof. split; last by case; [apply:BZps_sBZ | apply:BZm_sBZ]. case /BZ_i1P; [by move => ->; right; apply /setU1_P;right | by left | right ]. by apply /setU1_P;left. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)