proposition: Lemma set_meet_ubound S : set_meet (ubound S) = set_join S.
proof: Proof. apply/esym/set_meet_unique; [exact: set_join_le_ub|]. by move=> y; apply; apply: set_join_ub. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)