proposition: Lemma CS_beth x: ordinalp x -> cardinalp (beth x).
proof: Proof. move: (beth_prop) => [pa pb pc] ox. case: (least_ordinal6 (fun z => cardinalp (beth z)) ox) => //. set y := least_ordinal _ _;move=> [pd pe]; case. case: (ordinal_limA pd). - move ->; rewrite pb; apply: CS_omega. - move => [z oz za]; rewrite za pc; fprops. - by move /(proj2 pa) => ->; apply: CS_sup => t /funI_P [z zy ->]; apply: pe. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)