proposition: Theorem BZ_principal x: BZ_ideal x -> nonempty x -> exists2 a, inc a BZp & BZ_ideal1 a = x.
proof: Proof. move => ix nex. case: (p_or_not_p (exists2 a, inc a x & a <> \0z)); last first. move => h; exists \0z; first by apply: ZpS0. set_extens t. move:nex => [q qx]; move: (proj33 ix _ _ qx ZS0); rewrite BZprod_0r => tx. by move /BZ_ideal_0P => ->. move => tx; apply /BZ_ideal_0P; ex_middle xnz; case: h;ex_tac. move=> [a ax anz]. set (Z:= BZps \cap x). have pa: sub Z BZp by move => t /setI2_P [ta _]; apply: BZps_sBZp. have pb: nonempty Z. exists (BZabs a); apply/setI2_P; split; last by apply:BZ_idealS_abs. apply /zlt0xP; exact: (BZabs_positive (proj31 ix _ ax) anz). move: (BZ_N_worder pa pb) => [b bz bm]. move /setI2_P: bz => [] /BZps_iP [bzp bnz] bx; ex_tac. move: (BZp_sBZ bzp) => bz. set_extens t. move/funI_P => [u uz ->]; apply: (proj33 ix _ _ bx uz). move => tx. move: (BZ_idealS_rem ix tx bx) => rx. move: (BZdvd_correct (proj31 ix _ tx) bz bnz). move => [qa qb [qc qd qe]]. case: (equal_or_not (t %%z b) \0z) => tnz. move: (ZSp bz qa) => pz. rewrite qc tnz (BZsum_0r pz); apply /funI_P; exists (t %/z b) => //. have rz: inc (t %%z b) Z by apply /setI2_P; split => //; apply /BZps_iP. move:qd (bm _ rz);rewrite (BZabs_pos bzp) => la lb; BZo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)