proposition: Lemma beth_limit a: limit_ordinal a -> exists2 b, limit_ordinal b & beth a = \aleph b.
proof: Proof. move => la. have oa := proj31 la. move/limit_ordinal_P:la => [ap al]. move: (ord_index_pr1 (beth_pr1 oa)); set b := ord_index _; move => [ob bv]. case: (ordinal_limA ob) =>lb. - by case:(proj2 (beth_M ap)); move: bv; rewrite lb aleph0E - beth0. - move:lb => [c oc cv]. move:bv; rewrite cv => ea. move: (aleph_and_beth oc) => [d [od ha hb]]. move: (cle_ltT ha (aleph_lt_ltc (oltS oc))); rewrite ea => la. case: (oleT_ell oa od) => lb. by case: (proj2 la); rewrite lb. by case : (cltNge la (proj1(beth_M lb))). case: (cltNge (beth_M (al _ (al _ lb)))). move: (cleT (aleph_pr12f oc) (cpow_M2le (proj1 hb))). by rewrite ea - (beth_succ (OS_succ od)). - by exists b. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)