proposition: Lemma universe_inaccessible x a : inaccessible a -> inc x (universe a) -> cardinal x <c a.
proof: Proof. move => ia. have ica := (proj1 (proj1 (proj1 ia))). have oa:=(proj1 (proj1 ica)). move /(universe_P oa) => [b lba s1]. have ob := (proj31_1 lba). move: (beth_inaccessible ia lba). move: (sub_trans s1 (universe_inc2 (osum_M0le OS_omega ob))). move => /sub_smaller; rewrite (card_universe ob); apply:cle_ltT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)