proposition: Lemma cofinality_pr3 a: ordinalp a -> \cf a <=o a.
proof: Proof. move=> oa; move: (cofinality_rw oa) => [p1 p2 p3]. exact: (p3 _ oa (cofinal_function_pr2 oa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)