proposition: Lemma ord_sup_sub' X: ordinal_set X -> (inc (\osup X) X) \/ sub X (\osup X).
proof: Proof. move/oset_sub_ordinal => XS; case:(inc_or_not (\osup X) X) => h; first by left. right => t tX; case/setU1_P: (XS _ tX) => // tu; case:h; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)