proposition: Lemma set_meetU S S' : set_meet (setU S S') = meet (set_meet S) (set_meet S').
proof: Proof. apply/le_anti; rewrite meet_ge ?set_meetU_le_l ?set_meetU_le_r//. by rewrite set_meetU_ge ?meet_le_l ?meet_le_r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)