proposition: Lemma induced_sub_pr1 r X x: (forall a b, gle r a b -> sub a b) -> upper_bound r X x -> sub (union X) x.
proof: Proof. move=> h [xs ub] t /setU_P [y ty yX]. by apply: (h _ _ (ub _ yX)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)