proposition: Lemma set_meet2 x y : set_meet [set x; y] = x `&` y.
proof: Proof. apply/le_anti; rewrite set_meetU_ge ?set_meet1 ?leIl ?leIr//. rewrite lexI -[leRHS](set_meet1 x) set_meetU_le_l /=. by rewrite -[leRHS](set_meet1 y) set_meetU_le_r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)