proposition: Lemma osuccVpred x: ordinalp x -> osuccp x \/ x = opred x.
proof: Proof. move => ox; move: (opred_le ox) => la. case: (equal_or_not x (opred x)) => h; [ by right | left; exists (opred x) ]. apply: (proj31 la). apply: oleA; last by move/oleSltP: (conj la (nesym h)). split => //; [ exact: (OS_succ (proj31 la)) | move => t tx]. by move /oltSleP: (ord_sup_ub (Os_ordinal ox) tx) => /olt_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)