proposition: Lemma join_ub_3_assoc_m x y z : y ≤ x ⊔ (y ⊔ z).
proof: Proof. transitivity (y ⊔ z). - apply join_ub_l. - apply join_ub_r. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.semirings HoTT.Classes.theory.lattices