[Agda] add <-antysym to IsStrictPatialOrder ?

[Sergei Meshveliani]

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) ?

These two items are often used. And it looks like the most natural place
for them to appear.
(?)

Regards,

------
Sergei