proposition: Lemma finite_subset_directed_bounded r X: right_directed r -> finite_set X -> nonempty X -> sub X (substrate r) -> bounded_above r X.
proof: Proof. move=> [or rr]. apply: finite_set_induction3 => //; last by move => Y x Ysr neY [sr uYx]. move=> a b x y asr bsr [xsr ubx] [yser upy]. split =>//. have xy := (upy _ (set2_1 x b)). have lyb:= (upy _ (set2_2 x b)). move=> t /setU1_P; case; last by move=>->. move => ta; move: (ubx _ ta)=> aux; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)