proposition: Lemma set_joinU S S' : set_join (S `|` S') = set_join S `|` set_join S'.
proof: Proof. apply/le_anti; rewrite set_joinU_le ?leUl ?leUr//. by rewrite leUx set_joinU_ge_l set_joinU_ge_r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)