proposition: Lemma CS_cofinality x: ordinalp x -> cardinalp (\cf x).
proof: Proof. move => ox. move: (cofinality_rw ox) => [pa [g [[fg sg tg] gc]] pc]; split => //. move=> z oz e; move: (EqS e)=> [f [[[ff _] sjf] sf tf]]. suff H: (cofinal_function_ex x z) by exact (proj33 (pc _ oz H)). have cop: g \coP f by split => //; ue. exists (g \co f); split; first by red; saw; fct_tac. move => t tx; move: (gc _ tx) => [u]; rewrite -tf => utf tu. move: ((proj2 sjf) _ utf) => [v vsf vv]. rewrite - sf; ex_tac; rewrite compfV//; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)