proposition: Lemma universe_omega_props x: inc x (universe omega0) -> [/\ finite_set x, sub x (universe omega0) & inc (urank omega0 x) Nat].
proof: Proof. have aux:= card_universe_fin. move => xo. move:(xo);rewrite {1} (universe_limit omega_limit) => /setUf_P []. move => n nN etc; move:(OS_nat nN) => on. split. move: (universe_inc2 (proj1 (oltS on)) etc). rewrite (universe_succ on); move /setP_P => sn. apply:(sub_finite_set sn (aux _ nN)). by apply: (universe_trans OS_omega). move: (urank_pr1 on etc) => [[pa _] pb]. rewrite (urank_uniq2 OS_omega on xo etc). apply/(oltP OS_omega). move /(oltP OS_omega): nN; by apply: (ole_ltT). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)