proposition: Lemma osups_max X x: ordinalp x -> (forall y, inc y X -> y <=o x) -> inc x X -> osups X = osucc x.
proof: Proof. move => ox xp xX. have osX: ordinal_set X by move => t /xp /proj31. by rewrite /osups (oleA (ord_ub_sup ox xp) (ord_sup_ub osX xX)); Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)