proposition: Lemma cofinality'_pr3 r z (y:= (intersection (cofinality' r))): worder r -> sub z (substrate r) -> cofinal r z -> y <=o ordinal (induced_order r z).
proof: Proof. move=> wor zx cf. move: (cofinality'_pr0 wor) => [pa pb]. move: (ordinal_setI pa pb) => ys. set t := (ordinal (induced_order r z)). have wot : worder (induced_order r z) by apply: induced_wor. have ti: inc t (cofinality' r). apply /funI_P; exists z => //; apply: Zo_i => //; by apply /setP_P. split;fprops; by apply: setI_s1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)