proposition: Lemma meet_join_distr_l_le x y z : (x ⊓ y) ⊔ (x ⊓ z) ≤ x ⊓ (y ⊔ z).
proof: 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.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.semirings HoTT.Classes.theory.lattices