proposition: Lemma ord_ub_sup E y: ordinalp y -> ordinal_ub E y -> \osup E <=o y.
proof: Proof. move => oy h; split => //. by apply:OS_sup => i /h /proj31. by move=> i /setU_P [z iz /h [_ _]]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)