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