proposition: Lemma cofinality'_pr0 r : worder r -> (nonempty (cofinality' r) /\ ordinal_set (cofinality' r)).
proof: Proof. move => wor; move: (wor) => [or _]. set x := substrate r. have cx: cofinal r x. by split => // t tx; exists t => //; order_tac. have ior: (induced_order r x) = r by apply: iorder_substrate. split. exists (ordinal r); apply /funI_P; exists x; last by ue. apply: Zo_i; [ by aw; apply: setP_Ti | by rewrite ior]. move=> t /funI_P [z pa ->]; apply: OS_ordinal;apply: induced_wor => //. by move: pa => /Zo_P [] /setP_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)