proposition: Lemma BZ_in_ideal3 a: intp a -> BZ_ideal1 a = BZ_ideal2 a a.
proof: Proof. move: ZS0 => z0 az; set_extens t. move /funI_P => [x xz ->]; apply /Zo_P; split; first by apply: ZSp. by exists x, \0z;split => //; rewrite BZprod_0r BZsum_0r//; apply:ZSp. move=> /Zo_P [xz [u [v [uz vz pa]]]]; apply /funI_P. by exists (u +z v); [ apply:ZSs | rewrite (BZprodDr az uz vz) pa]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)