proposition: Lemma beth_dominant a: limit_ordinal a -> card_dominant (beth a).
proof: Proof. move => la; have oa:= (proj31 la). apply: (card_dominant_pr12 (beth_pr1 oa)). move => m /ord_index_pr1; set c := ord_index _; move => [oc <- lt0]. move: (aleph_and_beth oc) => [b [ob lt1 lt2]]. move/limit_ordinal_P:la => [anz sa]. have lt3: b <o a. have la4:= (cle_ltT lt1 lt0). case: (oleT_ell oa ob) => //. by move => ba; move: (proj2 la4); rewrite ba. move/beth_M => /cltNge; case; exact (proj1 la4). move: (cpow_M2le (proj1 lt2)); rewrite - (beth_succ (OS_succ ob)) => sb. by apply: (cle_ltT sb); apply:beth_M; apply: (sa); apply:sa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)