proposition: Lemma beth_dominantP x: infinite_c x -> (card_dominant x <-> exists2 a, (a = \0c \/ limit_ordinal a) & x = beth a).
proof: Proof. move => icx;split; last first. move => [a oa ->]; case: oa=> oa; last by apply:beth_dominant. by rewrite oa beth0; apply:card_dominant_pr2. move/ord_index_pr1: icx; set c := ord_index _; move => [oc <- xd]. move:(aleph_and_beth oc) => [b [ob lt1 lt2]]. have lt4:= (clt_fin_inf finite_2 (proj1 xd)). case: (equal_or_not (beth b) (\aleph c)) => eqa; last first. have lt3 : beth b <c \omega c by split. move: (proj2 xd _ _ lt4 lt3); rewrite - (beth_succ ob) => /cltNge; case. exact (proj1 lt2). exists b => //; case: (ordinal_limA ob) => lb; [by left | | by right]. move: lb => [d od bv]. have lc: d <o b by rewrite bv; apply: (oltS od). move: (beth_M lc); rewrite eqa => lt3. by move: (proj2 (proj2 xd _ _ lt4 lt3)); rewrite -(beth_succ od) - bv eqa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)