proposition: Lemma countable_ordinal_sup E: countable_set E -> (alls E countable_ordinal)-> countable_ordinal (\osup E).
proof: Proof. move: CIS_omega aleph_oneP => h T. move => /countableP pa pb. have se:sub E aleph_one by move => t /pb /T. by move /T: (cnext_sup h pa se). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)