proposition: Lemma join_ub_3_assoc_r x y z : z ≤ x ⊔ (y ⊔ z).
proof: Proof. transitivity (y ⊔ z); now apply join_ub_r. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.maps MathClasses.theory.lattices