proposition: Lemma osup_ub X x: ordinal_set X -> inc x X -> x <o osups X.
proof: Proof. move => ha hb. move: (ord_sup_ub ha hb); rewrite /osups; Ytac hc; first by move/oltSleP. by move => lex; split => // eq; case : hc; rewrite - eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)