proposition: Lemma join_le_compat x₁ x₂ y₁ y₂ : x₁ ≤ x₂ -> y₁ ≤ y₂ -> x₁ ⊔ y₁ ≤ x₂ ⊔ y₂.
proof: Proof. intros E1 E2. transitivity (x₁ ⊔ y₂). - apply (order_preserving (x₁ ⊔)). trivial. - apply (order_preserving (⊔ y₂));trivial. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.semirings HoTT.Classes.theory.lattices