proposition: Lemma z_omega_rec (p: property): p \0o -> (forall x, inc x z_omega -> p x -> p (osucc x)) -> forall x, inc x z_omega -> p x.
proof: Proof. move => P0 Hrec. set E := Zo z_omega p. move: z_omega_prop => [[qa qb] qc]. have /qc s: z_infinite E. split; [apply:Zo_i | move => x /Zo_P [ ra rb]; apply: Zo_i]; fprops. by move => x /s/Zo_hi. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)