proposition: Lemma cofinality_rw a (b:= \cf a) : ordinalp a -> [/\ ordinalp b, cofinal_function_ex a b & forall z, ordinalp z -> cofinal_function_ex a z -> b <=o z].
proof: Proof. set p := cofinal_function_ex a. move=> oa. have pa: p a by apply: cofinal_function_pr2. move: (least_ordinal1 oa pa) => [pb pc pd];split => // z oz pz; split;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)