proposition: Lemma iclosed_non_coll_infinite_c: iclosed_proper infinite_c.
proof: Proof. have H: ordinal_prop infinite_c by move => x [[oc _]_]. split; first split => //. move => F iF [y yF]. have cs: cardinal_set F by move => z /iF []. exact: (cle_inf_inf (iF _ yF) (card_sup_ub cs yF)). apply: unbounded_non_coll => //. move => x ox; case: (oleT_ee ox OS_omega) => cxo. exists omega0 => //; apply: CIS_omega. have aux: cardinal x <c \2c ^c x by rewrite - cpowcr; apply: cantor; fprops. move /infinite_setP:(infinite_set_pr3 cxo) => hh. move: (cle_inf_inf hh (proj1 aux)) => aux2. move /(ocle2P (proj1 aux2) ox): aux => [aux3 _]. by exists (\2c ^c x). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)