proposition: Lemma oprod2_countable a b: countable_ordinal a -> countable_ordinal b -> countable_ordinal (a *o b).
proof: Proof. move: CIS_omega aleph_oneP => h T. by move => /T xa /T xn; apply /T;apply:cnext_prod. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)