proposition: Lemma countable_succ a: countable_ordinal a -> countable_ordinal (osucc a).
proof: Proof. move=> cx; move: (cx) => [ox _]; rewrite - (osucc_pr ox). apply: osum2_countable => //; apply: countable_one. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)