proposition: Lemma urank_ordinal x: ordinalp x -> urank_prop x x.
proof: Proof. move => ox; split; first exact. apply: (ordinal_in_universe ox). move => c cx /setP_P. move: (universe_inc1 cx) => qa qb; move: (qa _ qb) => xx. move: (least_ordinal4 ox xx (p:= fun y => inc y (universe y))). simpl; set a := least_ordinal _ _; move => [oa nzz rec]. move /(universe_P oa): nzz => [b ba bb]; apply: (oleNgt _ ba). apply:rec; first exact: (proj31_1 ba). by apply: bb; apply /(oltP oa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)