proposition: Lemma oset_sub_ordinal X: ordinal_set X -> sub X (osucc (\osup X)).
proof: Proof. move => ose t tX. by apply/(ordinal_sub4P (ose t tX) (OS_sup ose)); apply: (setU_s1 tX). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)