IsMeetSemiLattice L. Proof. repeat split. - apply _. - intros x y z. apply (antisymmetry (≤)). + apply meet_glb. * apply meet_glb. ** apply meet_lb_3_assoc_l. ** apply meet_lb_3_assoc_m. * apply meet_lb_3_assoc_r. + apply meet_glb. ** apply meet_lb_3_l. ** apply meet_glb. *** apply meet_lb_3_m. *** apply meet_lb_3_r. - intros x y. apply (antisymmetry (≤)); apply meet_glb; first [apply meet_lb_l | try apply meet_lb_r]. - intros x. red. apply (antisymmetry (≤)). + apply meet_lb_l. + apply meet_glb;apply reflexivity. Qed.
Require Import