proposition: Lemma set_join_lbound S : set_join (lbound S) = set_meet S.
proof: Proof. apply/esym/set_join_unique; [exact: set_meet_ge_lb|]. by move=> y; apply; apply: set_meet_lb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)