proposition: Lemma limit_nonsucc x: limit_ordinal x -> x = opred x.
proof: Proof. move => [ox zx sx]. case: (osuccVpred ox) => // [] [y oy xy]. have yx: (inc y x) by rewrite xy; fprops. by move: (sx _ yx); rewrite -xy => /(ordinal_irreflexive ox). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)