proposition: Lemma BZps_iP x: inc x BZps <-> (inc x BZp /\ x <> \0z).
proof: Proof. split. move => /indexed_P [pa ] /setC1_P [pb pc] pd;split => //. by apply /indexed_P. by dneg pe; rewrite pe BZ0_val. move => [] /indexed_P [pa pb pc] pd; apply /indexed_P;split => //. apply /setC1_P;split => //. dneg pe;rewrite /BZ_zero /BZ_of_nat; apply: pair_exten;aww. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)