proposition: Lemma cofinality'_pr1 r: total_order r -> (nonempty (cofinality' r) /\ ordinal_set (cofinality' r)).
proof: Proof. move => tor; rewrite /cofinality'. move: (Exercise6_16a tor) => [X ta tb]. split. exists (ordinal (induced_order r X)); apply /funI_P; exists X => //. by apply: Zo_i => //; move: ta => [tc _]; apply /setP_P. move=> x => /funI_P [z szf ->]; apply: OS_ordinal. by move: szf => /Zo_hi [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)