proposition: Lemma cofinality_reg x: ordinalp x -> regular_ordinal (\cf x).
proof: Proof. move=> ox; move: (OS_cofinality ox) => ofx. split => //; apply: (cofinality_proj ox). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)