proposition: Lemma join_le x y z : x ≤ z → y ≤ z → x ⊔ y ≤ z.
proof: Proof. intros. rewrite <-(idempotency (⊔) z). now apply join_le_compat. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.maps MathClasses.theory.lattices