proposition: Lemma cofinal_function_pr2 a: ordinalp a -> cofinal_function_ex a a.
proof: Proof. move=> oa; exists (identity a); split; first by red; aw;split;fprops. move=> x xa; exists x => //; rewrite idV //. exact: (oleR (Os_ordinal oa xa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)