proposition: Lemma OS_urank x a: ordinalp a -> ordinalp (urank a x).
proof: Proof. move => oa; rewrite /urank /least_ordinal; set S := Zo _ _. case: (emptyset_dichot S) => h; first by rewrite h setI_0; fprops. have os: ordinal_set S. move => t /Zo_S /setU1_P[] ta; [exact: (Os_ordinal oa ta) | ue ]. exact: (os _ (ordinal_setI h os)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)