proposition: Lemma set_meetU S S' : set_meet (S `|` S') = set_meet S `&` set_meet S'.
proof: Proof. apply/le_anti; rewrite set_meetU_ge ?leIl ?leIr//. by rewrite lexI set_meetU_le_l set_meetU_le_r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)