[Agda] add <-antysym to IsStrictPatialOrder ?

[Nils Anders Danielsson]

On 2013-09-29 14:47, Sergei Meshveliani wrote:
> Has it sense to add to  IsStrictPatialOrder  this:
>
>    _≮_ : Rel A _
>    x ≮ y =  ¬ x < y
>
>    <-antisym : {x y : A} → x < y → y ≮ x
>    <-antisym x<y =  irrefl ≈refl ∘ <-trans x<y
>
> (one definition and one lemma) ?

I've added asymmetric : Asymmetric _<_.

-- 
/NAD