proposition: Lemma urank0_pr3 a b: universe_i b -> inc a b -> urank0 a <o urank0 b.
proof: Proof. move => [c oc bc] iab. move:(urank0_pr oc bc) => [-> _]. move:(urank_inc oc bc iab) => [sc sd]. by move:(urank0_pr oc sc) => [-> _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)