proposition: Lemma cofinality_index a: ordinalp a -> ord_index (\cf (\omega a)) <=o a.
proof: Proof. move=> on; move: (CIS_aleph on) => io. move: (cofinality_pr3 (proj1 (proj1 io))). move: (cofinality_infinite io). rewrite (cofinality_card io) =>pa pd. move: (ord_index_pr1 pa) => [pb pc]. by apply: aleph_leo_le => //; rewrite pc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)