[Agda] Equality in strict total order

[cyberfined]

Hi, everyone. I need to prove that if x ≈ y and y < z, then x < z. But i can't use a rewrite, because x ≈ y is not the same as x ≡ y. So, my question is: how can i prove it?

open import Relation.Binary using (StrictTotalOrder)

module Test
{a 𝓁₁ 𝓁₂} (strictTotalOrder : StrictTotalOrder a 𝓁₁ 𝓁₂) where

open StrictTotalOrder strictTotalOrder renaming (Carrier to A)

x≈y∧y<z⇒x<z : ∀ {x y z : A} → x ≈ y → y < z → x < zx≈y∧y<z⇒x<z x≈y x<z = ?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220723/0b4d44e7/attachment.html>