proposition: Lemma set_joinU_ge_l S S' : set_join S <= set_join (S `|` S').
proof: Proof. exact/set_join_le_ub/set_joinUl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)