proposition: Lemma z_omega_prop : z_infinite z_omega /\ forall E, z_infinite E -> sub z_omega E.
proof: Proof. have nez: nonempty (Zo (\Po E0) z_infinite). by exists E0; apply:Zo_i => //; apply/setP_P. have Ho: z_infinite z_omega. split; first by apply/(setI_P nez) => i /Zo_P [ _ []]. move => x xo;apply/(setI_P nez) => i iZ; move:(iZ)=> /Zo_P [ _ [_]]; apply. exact: (setI_hi xo iZ). split => // E iE; apply: sub_trans (@setI2_1 E E0). apply: setI_s1; apply:Zo_i; first by apply/setP_P; apply:setI2_2. move: HE iE =>[pa pb][pc pd]. split. fprops. move => t /setI2_P [/pd qd /pb qb]; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)