proposition: Lemma meet_le_compat x₁ x₂ y₁ y₂ : x₁ ≤ x₂ → y₁ ≤ y₂ → x₁ ⊓ y₁ ≤ x₂ ⊓ y₂.
proof: Proof. intros E1 E2. transitivity (x₁ ⊓ y₂). now apply (order_preserving (x₁ ⊓)). now apply (order_preserving (⊓ y₂)). Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.maps MathClasses.theory.lattices