proposition: Lemma set_joinUr S S' : ubound S' (set_join (S `|` S')).
proof: Proof. rewrite setUC; exact: set_joinUl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)