x₁ x₂ y₁ y₂ : x₁ ≤ x₂ -> y₁ ≤ y₂ -> x₁ ⊔ y₁ ≤ x₂ ⊔ y₂. Proof. intros E1 E2. transitivity (x₁ ⊔ y₂). - apply (order_preserving (x₁ ⊔)). trivial. - apply (order_preserving (⊔ y₂));trivial. Qed.
Require Import