Adding `DecStrictPartialOrder` to Relation.Binary

Most orderings in Relation.Binary have a decidable variation. Three notable exceptions are Preorder, StrictPartialOrder and StrictTotalOrder (though the last of these is decidable in itself, by virtue of the `compare` function).

My commit adds implementations of DecStrictPartialOrder and IsDecStrictPartialOrder, and was tested against the HEAD version of Agda.