proposition: Lemma join_meet_distr_l_le x y z : x ⊔ (y ⊓ z) ≤ (x ⊔ y) ⊓ (x ⊔ z).
proof: Proof. apply meet_le. apply join_le. now 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.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.maps MathClasses.theory.lattices