x y z : (x ⊓ y) ⊔ (x ⊓ z) ≤ x ⊓ (y ⊔ z). Proof. apply meet_le. - apply join_le; apply meet_lb_l. - apply join_le. + transitivity y. * apply meet_lb_r. * apply join_ub_l. + transitivity z. * apply meet_lb_r. * apply join_ub_r. Qed.
Require Import