proposition: Lemma z_omega_infinite2: z_omega \Eq (osucc z_omega).
proof: Proof. move: z_omega_infinite; set f := Lf _ _ _; move => [[fi sf tf] pb]. move: (restriction_to_image_fb fi) => bf. move:(ordinal_irreflexive (z_omega_ordinal)) z_omega_prop => ha /proj1/proj1 hd. have hb: ~ inc \0o (Imf f) by rewrite pb => /setC1_P[]. move: (succ_inf_aux_p1 ha hb). rewrite {2} pb (setC1_K hd) => h. apply: EqS; apply: h. exists (restriction_to_image f). by split => //; rewrite /restriction_to_image/restriction2; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)