proposition: Lemma z_omega_ordinal: ordinalp z_omega.
proof: Proof. apply: ordinal_pr. apply:z_omega_rec; first by move => t/in_set0. by move => x pa pb; apply: setU1_sub. by apply:(z_omega_rec OS0) => x _ /OS_succ. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)