proposition: Lemma cofinality_pr1 x (r:= ordinal_o x): ordinalp x -> (exists z, [/\ sub z x, cofinal r z, worder (induced_order r z) & cofinality_alt x = ordinal (induced_order r z)]).
proof: Proof. move => /ordinal_o_wor; rewrite -{2} (ordinal_o_sr x); apply:cofinality'_pr2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)