proposition: Lemma cofinality_proj x: ordinalp x -> \cf (\cf x) = \cf x.
proof: Proof. move=> ox; move: (OS_cofinality ox) => ofx. apply: (cofinality_pr5 ofx ox). by move: (cofinality_pr4 ox) => [f [ff [_ si _ _]]]; exists f. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)