proposition: Lemma succo_K y: ordinalp y -> opred (osucc y) = y.
proof: Proof. move=> oy; set_extens t => ts; last by apply: (setU_i ts); fprops. move: (setU_hi ts) => [a ta]; case /setU1_P;last by move => <-. move => ay;exact:(ordinal_transitive oy ay ta). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)