proposition: Lemma posnat_ordinalp x : posnatp x <-> (\0o <o x /\ x <o omega0).
proof: Proof. split; move => [ha hb]. split;[ apply:(oclt hb) | by apply/olt_omegaP]. apply:posnat_prop; [ by apply /olt_omegaP |exact (nesym (proj2 ha))]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)