proposition: Lemma cofinality_index_regular a (x :=\omega a) : ordinalp a -> (regular_ordinal x <-> ord_index (\cf x) = a).
proof: Proof. move=> on;split; first by move => [pa ->]; apply: ord_index_pr. move => pa; split; first by apply: OS_aleph. rewrite /x - {2} pa. have ic: infinite_c (\cf (\omega a)). by apply: cofinality_infinite_cardinal; apply: CIS_aleph. by move: (ord_index_pr1 ic) =>[_ ->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)