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₂). - 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