# [Agda] Equality in strict total order

James Wood james.wood.100 at strath.ac.uk
Sat Jul 23 14:21:33 CEST 2022

```Hi, I believe you're looking for <-respˡ-≈ , which is in scope thanks to
having opened StrictTotalOrder (via a very long chain of open ...
publics, I imagine). There's an interactive editing command for finding
stuff like this: In Emacs, C-c C-o StritTotalOrder.

All the best,
James

On 23/07/2022 12:23, cyberfined wrote:
> CAUTION: This email originated outside the University. Check before
> 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 < z
> x≈y∧y<z⇒x<z x≈y x<z = ?
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

```