proposition: Lemma BZ_ideal_0P a: inc a (BZ_ideal1 \0z) <-> (a = \0z).
proof: Proof. split; first by move => /funI_P [z]; rewrite BZprod_0l. by move => ->; apply /funI_P; exists \0z; [ apply: ZS0 |rewrite BZprod_0r]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)