proposition: Lemma cofinality_limit_countable x: limit_ordinal x -> countable_ordinal x -> \cf x = omega0.
proof: Proof. move => ha [hb /countableP hc]; apply: oleA. move: (ocle (cleT (ocle1 (cofinality_pr3 hb)) hc)). by rewrite (card_card(CS_cofinality hb)). exact:(limit_ge_omega (cofinality_limit3 ha)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)