proposition: Lemma urank_inc a x y : ordinalp a -> inc x (universe a) -> inc y x -> inc y (universe a) /\ (urank a y) <o (urank a x).
proof: Proof. move => oa xa yx. move: (urank_pr1 oa xa) => [_ [sa sb _]]. move: (universe_trans oa xa yx) => ya; split => //; apply /oleSltP. have ysa:= (universe_trans oa ya). move: (sb _ yx) => h; move: (urankA_pr sa h)=> [pc pd]. by rewrite - (urank_alt1 oa ya) - (urankA_uniq pd (proj2 (urankA_pr oa ya))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)