proposition: Lemma ordinal_limA x: ordinalp x -> [\/ x = \0o, osuccp x | limit_ordinal x].
proof: Proof. move=> ox. case: (emptyset_dichot x); first by constructor 1. move=> nex. case: (osuccVpred ox); first by constructor 2. by move=> xu; constructor 3; apply /(limit_ordinal_P0 ox). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)