proposition: Lemma cofinality_c_of0: cofinality_c \0c = \0c.
proof: Proof. rewrite /cofinality_c /least_ordinal; set E := Zo _ _. case: (emptyset_dichot E) => h; first by rewrite h; exact setI_0. apply/set0_P => t tiE; move: h => [y ye];move:(setI_hi tiE ye). move/Zo_P:ye => [_] [f [[_ ha] hb hc]]. rewrite - hb;case: (emptyset_dichot (domain f)); first by move => -> /in_set0. by move => [i /ha /clt0]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)