proposition: Lemma set_meetU_ge S S' x : x <= set_meet S -> x <= set_meet S' -> x <= set_meet (S `|` S').
proof: Proof. move=> xmS xmS'; apply: set_meet_ge_lb => y [] Sy. - exact/(le_trans xmS)/set_meet_lb. - exact/(le_trans xmS')/set_meet_lb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)