proposition: Lemma limit_ordinal_P0 x: ordinalp x -> ((limit_ordinal x) <-> (nonempty x /\ x = opred x)).
proof: Proof. move=> ox; split. move => lx; move:(limit_nonsucc lx) => sa; split => //. by move: (proj32 lx) => zx; exists emptyset. move => [/nonemptyP nex ww]. apply/limit_ordinal_P; split. exact: (ord_ne0_pos ox nex). move => t /oleSltP h; split => // h'. have osx: osuccp x by exists t=> //; apply: OS_succr; ue. exact: (osuccNpred osx ww). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)