proposition: Lemma urank_sub a x y : ordinalp a -> inc x (universe a) -> sub y x -> inc y (universe a) /\ (urank a y) <=o (urank a x).
proof: Proof. move => oa xa yx. move:(urank_pr1 oa xa) =>[pa pb];move: (pb) => [p1 p2 p3]. have pc: inc y (universe (osucc (urank a x))). rewrite (universe_succ p1); apply /setP_P; apply: (sub_trans yx p2). have p4: (osucc (urank a x)) <=o a by apply /oleSltP. have ya: inc y (universe a) by apply:(universe_inc2 p4). move: (urank_pr1 (OS_succ p1) pc) => []. by rewrite (urank_uniq2 (OS_succ p1) oa pc ya) => /oltSleP h _. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)