proposition: Lemma CIS_aleph x: ordinalp x -> infinite_c (\aleph x).
proof: Proof. move: iclosed_non_coll_infinite_c => [ [pa _] pb]. by move:(ordinals_col_p1 pa pb) => [h _ _ _ _]; apply: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)