proposition: Lemma set_meetU_is_glb : set_f_is_glb set_meetU.
proof: Proof. move=> B; split. - by move=> x Bx; rewrite leEsub subK set_meet_lb//; exists x. - move=> x ubx; rewrite leEsub subK set_meet_ge_lb// => _ [y By <-]. by rewrite -leEsub ubx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)