proposition: Lemma z_omega_infinite (f := Lf osucc z_omega z_omega): injection_prop f z_omega z_omega /\ Imf f = z_omega -s1 \0o.
proof: Proof. move: z_omega_prop z_omega_ordinal =>[ [qa qb] qc] oo. have H: injection_prop f z_omega z_omega. rewrite /f; saw; apply: lf_injective => //. by move => u v ua uv; apply: osucc_inj; apply: (Os_ordinal oo). move: (H) => [[ff injf] sf tf]. have/qc ii: z_infinite ((Imf f) +s1 \0o). split; fprops => x /setU1_P hh; apply: setU1_r;apply/(Imf_P ff). rewrite sf /f; case: hh; last by move ->; exists \0o => //;rewrite LfV. by move/(Imf_Starget ff); rewrite tf => xo; ex_tac; rewrite LfV. split => //; set_extens t. move/(Imf_P ff) =>[u usf ->]; apply/setC1_P; rewrite /f; rewrite sf in usf. rewrite LfV //; split; fprops; rewrite/ord_zero => h; empty_tac1 u. by move => /setC1_P [/ii /setU1_P to tnz]; case: to. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)