proposition: Lemma urank_pr1 x a (b:= urank a x): ordinalp a -> inc x (universe a) -> b <o a /\ urank_prop x b.
proof: Proof. move => oa xa. move:(urank_pr oa (universe_trans oa xa))=> [_ h]; split => //. move: (urankA_pr oa xa) => [h1 h2]; apply /oleSltP. by rewrite - (urank_alt1 oa xa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)