proposition: Lemma dominant_limit a: ordinalp a -> ~ (card_dominant (\aleph (osucc a))).
proof: Proof. move=> oa [cd1 cd2]. set x := \omega a. rewrite - (cnextE oa) in cd2. move: (CIS_aleph oa) => icx. move: (cnext_pr2 (proj1 icx))(cnext_pr3 (proj1 icx)) => lt1 pa. by move: (cd2 _ _ lt1 lt1); rewrite (infinite_power1_b icx) => /cltNge. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)