proposition: Lemma set_join2 x y : set_join [set x; y] = x `|` y.
proof: Proof. apply/le_anti; rewrite set_joinU_le ?set_join1 ?leUl ?leUr//. rewrite leUx -[leLHS](set_join1 x) set_joinU_ge_l /=. by rewrite -[leLHS](set_join1 y) set_joinU_ge_r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)