proposition: Lemma Exercise6_22c1 x: card_dominant x -> (x = omega0 \/ (exists2 n, limit_ordinal n & x = \aleph n)).
proof: Proof. move => [pa pb]. move: (ord_index_pr1 pa); set c := ord_index x; move => [pd pe]. case: (ordinal_limA pd) => ln;last by right; exists c. by left; rewrite -pe ln aleph0E. move: ln => [m om mv]. set y:= \aleph m. have yx: y <c x. by rewrite /y -pe; apply: aleph_lt_ltc; rewrite mv; apply: oltS. move: (pb _ _ yx yx); rewrite (infinite_power1_b (CIS_aleph om)) => le1. by move: (cnext_pr3(CS_aleph om));rewrite (cnextE om) -mv pe => /(cltNge le1). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)