proposition: Lemma ord_sup_M x y: sub x y -> ordinal_set y -> (\osup x) <=o (\osup y).
proof: Proof. move=> xy al1. apply:ord_ub_sup => //; first by apply: OS_sup. by move=> i ix; apply: ord_sup_ub => //; apply: xy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)