x : x ⊓ x = x. Proof. assert (le1 : x ⊓ x ≤ x). { refine (meet_lb_l _ _). } assert (le2 : x ≤ x ⊓ x). { refine (meet_glb _ _ _ _ _); apply reflexivity. } refine (antisymmetry _ _ _ le1 le2). Qed.
Require Import