proposition: Lemma Cantor_omega_pr x: inc x Cantor_Omega <-> (countable_ordinal x /\ omega0 <=o x).
proof: Proof. split. move /setC_P => [/aleph_oneP pa pb]; split => //. by case: (oleT_el OS_omega (proj1 pa)) => // /oltP0 [_ _]. move => [pa pb]; apply/setC_P; split; first by apply /aleph_oneP. by move => xo; move: (proj33 pb _ xo)(ordinal_irreflexive (proj32 pb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)