proposition: Lemma ord_sup_inVlimit X: ordinal_set X -> nonempty X -> inc (\osup X) X \/ limit_ordinal (\osup X).
proof: Proof. move=> alo [a aX]. case: (p_or_not_p (inc (\osup X) X)) => nsX; [ by left | right]. have asu:= (ord_sup_ub alo aX). have so:= proj32 asu. case: (ordinal_limA so) => //. by move=> h; rewrite h in nsX asu;case: nsX; rewrite - (ole0 asu). move => [y oy h]. have aiy: (forall i, inc i X -> i <=o y). move=> i iX; apply /oltSleP. by rewrite -h; apply: ord_sup_sub. move: (ord_ub_sup oy aiy); rewrite h. by move /oleSltP => [_ ?]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)