proposition: Lemma opow_countable x y: countable_ordinal x -> countable_ordinal y -> countable_ordinal (x ^o y).
proof: Proof. move: CIS_omega aleph_oneP => h T. by move => /T xa /T xn; apply /T;apply:cnext_pow. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)