<div style="font-family: Arial; font-size: 12px; color: rgb(0, 0, 0);">Hi, everyone. I need to prove that if <span>x ≈ y and y < z, then x < z.</span> But i can't use a rewrite, because x <span>≈</span> y is not the same as x <span>≡</span> y. So, my question is: how can i prove it?</div><div style="font-family: Arial; font-size: 12px; color: rgb(0, 0, 0);"><br></div><div style="font-family: Arial; font-size: 12px; color: rgb(0, 0, 0);"><span style="font-family: Menlo, Consolas, Courier New, monospace;">open import Relation.Binary using (StrictTotalOrder)</span><div><br></div><div><span style="font-family: Menlo, Consolas, Courier New, monospace;">module Test</span></div><div><span style="font-family: Menlo, Consolas, Courier New, monospace;">    {a 𝓁₁ 𝓁₂} (strictTotalOrder : StrictTotalOrder a 𝓁₁ 𝓁₂) where</span></div><div><br></div><div><span style="font-family: Menlo, Consolas, Courier New, monospace;">open StrictTotalOrder strictTotalOrder renaming (Carrier to A)</span></div><div><br></div><div><span style="font-family: Menlo, Consolas, Courier New, monospace;">x≈y∧y<z⇒x<z : ∀ {x y z : A} → x ≈ y → y < z → x < z</span></div><span style="font-family: Menlo, Consolas, Courier New, monospace;">x≈y∧y<z⇒x<z x≈y x<z = ?</span><br></div>