proposition: Lemma urankA_pr x a (b:= urankA a x): ordinalp a -> inc x (universe a) -> b <=o a /\ urankA_prop x b.
proof: Proof. move =>oa pa. pose p b := inc x (universe b). move: (least_ordinal4 oa pa (p:=p)) => []; rewrite -/(urank _ _) -/b /p. move => ob xb etc; split; first by apply: etc. split => //;move => c cb xc. case: (oltNge cb (etc _ (proj31_1 cb) xc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)