proposition: Lemma finite_preorder_directed_bounded r I E: preorder r -> substrate r = I -> right_directed_on r I-> nonempty E -> finite_set E -> sub E I -> exists2 x, inc x I & forall y, inc y E -> gle r y x.
proof: Proof. move=> or sr rdr ha hb hc. suff: exists x, forall y : Set, inc y E -> gle r y x. move => [x xp]; exists x => //; move:ha => [y yE]. move:(arg2_sr (xp _ yE)); ue. move: E hb ha hc; apply:(finite_set_induction3). - move => a b aI bI; move:(rdr _ _ aI bI) => [c [cI ca cb]]; exists c. by move => t /set2_P [] ->. - move => a b x y aI bI pa pxb t /setU1_P. move:(pxb _ (set2_1 x b)) (pxb _ (set2_2 x b)) => xy lyb. case; [ by move/pa => tx; apply: (proj33 or _ _ _ tx xy) | by move ->]. - by move => X x XI [a aX] h; move: (arg2_sr (h _ aX)); ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)