proposition: Lemma set_meetU_le_l S S' : set_meet (S `|` S') <= set_meet S.
proof: Proof. exact/set_meet_ge_lb/set_meetUl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)