diff --git a/Analysis/Utils.agda b/Analysis/Utils.agda
new file mode 100644
index 0000000..b87a3c8
--- /dev/null
+++ b/Analysis/Utils.agda
@@ -0,0 +1,15 @@
+module Analysis.Utils where
+
+open import Data.Product using (_,_)
+open import Lattice
+
+module _ {o} {O : Set o} {_≼ᴼ_ : O → O → Set o}
+         (≼ᴼ-trans : ∀ {o₁ o₂ o₃} → o₁ ≼ᴼ o₂ → o₂ ≼ᴼ o₃ → o₁ ≼ᴼ o₃)
+         (combine : O → O → O) (combine-Mono₂ : Monotonic₂ _≼ᴼ_ _≼ᴼ_ _≼ᴼ_ combine) where
+
+    eval-combine₂ : {o₁ o₂ o₃ o₄ : O} → o₁ ≼ᴼ o₃ → o₂ ≼ᴼ o₄ →
+                    combine o₁ o₂ ≼ᴼ combine o₃ o₄
+    eval-combine₂ {o₁} {o₂} {o₃} {o₄} o₁≼o₃ o₂≼o₄ =
+        let (combine-Monoˡ , combine-Monoʳ) = combine-Mono₂
+        in ≼ᴼ-trans (combine-Monoˡ o₂ o₁≼o₃)
+                    (combine-Monoʳ o₃ o₂≼o₄)