proposition: Lemma join_le x y z : x ≤ z -> y ≤ z -> x ⊔ y ≤ z.
proof: Proof. apply join_lub. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.semirings HoTT.Classes.theory.lattices