proposition: Lemma cofinality_regular x (y:= \cf x): ordinalp x -> [\/ y = \0c, y = \1c | regular_cardinal y].
proof: Proof. move => ox. move: (cofinality_reg ox); rewrite -/y => ry. case: (regular_finite ry); first by constructor 1. by constructor 2. move: (regular_is_cardinal ry) => cy iy. have icy: infinite_c y. by move /infinite_setP: (infinite_set_pr3 iy);rewrite card_card. constructor 3; split => //; rewrite (cofinality_card icy). exact (proj2 ry). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)