proposition: Lemma ordinals_of_universe a: ordinalp a -> Zo (universe a) ordinalp = a.
proof: Proof. move => oa; apply:extensionality; last first. move => t ta; apply/Zo_P; split; last exact:(Os_ordinal oa ta). exact:((ordinal_in_universe oa) _ ta). case: (least_ordinal6 (fun a => sub (Zo (universe a) ordinalp) a) oa) => //. set y := least_ordinal _ _; move => [oy hrec]; case. case: (ordinal_limA oy) => h. + by rewrite h universe_0 => t /Zo_S /in_set0. + move: h => [z oz zy] t /Zo_P [ts ot]. move: ts; rewrite zy (universe_succ oz) => /setP_P stz. apply/(oltP (OS_succ oz)) /oltSleP; split => // u ut. have izy: inc z y by rewrite zy; fprops. apply: (hrec _ izy); apply/Zo_P; split => //; first exact: (stz _ ut). exact: (Os_ordinal ot ut). move/limit_ordinal_P:(h) => [sa sb]. move => t/Zo_P [tut ot]. move:tut;rewrite (universe_limit h) => /setUf_P [z zy zv]. have :inc t (Zo (universe z) ordinalp) by apply/Zo_P. by move /(hrec _ zy); move:(ordinal_transitive oy zy); apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)