proposition: Lemma osups_ordinal a : ordinalp a -> osups a = a.
proof: Proof. move => oa; move:(ord_sup_ordinal oa); rewrite /osups. case => ha; first by rewrite - ha (Y_false (ordinal_irreflexive oa)). rewrite -ha Y_true // {2} ha; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)