[Agda] Equality in strict total order

[James Wood]

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 
> clicking links or attachments.
> 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