proposition: Lemma cofinality_c_of1: cofinality_c \1c = \0c.
proof: Proof. rewrite /cofinality_c /least_ordinal; set E := Zo _ _. case: (emptyset_dichot E) => h; first by rewrite h; exact setI_0. move: h => [y /Zo_P [_ [f[[fgf ha] hb]]]]. have ->:csum f = (csumb (domain f) (fun i =>\0c)). rewrite - csum_gr; apply: csumb_exten => i idf. by move: (clt1 (ha _ idf)). by rewrite csum_of_same cprod0l => lt; case: card1_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)