proposition: Lemma aleph_oneP a: inc a aleph_one <-> countable_ordinal a.
proof: Proof. move:(cnextP CS_omega) => h. split; first by move/h => [ha /countableP hb]. by move => [ha /countableP hb]; apply/h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)