proposition: Lemma set_joinU S S' : set_join (setU S S') = join (set_join S) (set_join S').
proof: Proof. apply/le_anti; rewrite set_joinU_le ?join_ge_l ?join_ge_r//. by rewrite join_le ?set_joinU_ge_l ?set_joinU_ge_r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)