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₄)