proposition: Lemma set_join_unique S x : ubound S x -> (forall y, ubound S y -> x <= y) -> x = set_join S.
proof: Proof. move=> xub xlub; apply/le_anti; rewrite set_join_le_ub // andbT. exact/xlub/set_join_ub. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)