proposition: Lemma integer_in_Vomega x: inc x (universe omega0) -> (inc x Nat <-> ordinal_altp x).
proof: Proof. move => xu. have hc: forall y, sub y x -> foundation_prop y. move => y yx;apply:universe_AF; exists omega0; first fprops. exact (proj1 (urank_sub OS_omega xu yx)). split; first by move/OS_nat => /(ordinal_with_AF hc). move /(ordinal_with_AF hc) => ox. move: (proj31(universe_omega_props xu)) => fsx. move: (card_card (CS_finite_o(ordinal_finite1 ox fsx))) => cx. by apply/NatP; rewrite - cx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)