proposition: Lemma ord_sup_ordinal a (b:= \osup a): ordinalp a -> a = b \/ a = osucc b.
proof: Proof. by move=> oa; case: (osuccVpred oa); [ move/predo_K; right | left ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)