proposition: Lemma set_join_is_lub : set_f_is_lub set_join.
proof: Proof. move=> B; split; [|exact: (set_meet_is_glb _).1]. by move=> x Bx; apply: (set_meet_is_glb _).2; move=> y; apply. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)