proposition: Lemma finite_pred x: finite_o x -> x <> \0o -> (exists2 y, finite_o y & x = osucc y).
proof: Proof. move => fx xnz. case: (ordinal_limA (proj1 fx)). - done. - move=> [y oy xK]; rewrite xK; exists y => //; apply/finite_sP;ue. - move => lim; case: (proj2 fx); apply: (OIS_limit lim). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)