proposition: Lemma set_meetUl S S' : lbound S (set_meet (S `|` S')).
proof: Proof. move=> y Sy; have: (S `|` S') y by left. move: y {Sy}; exact: set_meet_lb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)