proposition: Lemma cofinality'_pr2 r (y:= (intersection (cofinality' r))) : worder r -> (exists z, [/\ sub z (substrate r), cofinal r z, worder (induced_order r z) & y = ordinal (induced_order r z)]).
proof: Proof. move=> /cofinality'_pr0 [pa pb]. move: (ordinal_setI pa pb). rewrite /cofinality'; move=> /funI_P [z z1 z2]. by move: z1 => /Zo_P [pc [pd pe]]; exists z;split => //; apply /setP_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)