proposition: Lemma omega_rec (p: property): p \0o -> (forall x, inc x omega0 -> p x -> p (osucc x)) -> forall x, inc x omega0 -> p x.
proof: Proof. have ho: z_infinite omega0 by case: omega_limit. move: omega0_pr => [qc qd qe]. move: (z_omega_prop ho) (z_omega_ordinal ho) (z_omega_rec ho) => [qa qb] qf. rewrite - (extensionality (qe _ qf (z_omega_infinite2 ho)) (qb _ ho)). apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)