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