It is better to write
f p@(prep2 x y xs x<=y ord-y-xs) = prep2 0 x (y :: xs) z<=n p
than
f (prep2 x y xs x<=y ord-y-xs) = prep2 0 x (y :: xs) z<=n
(prep2 x y xs x<=y ord-y-xs)
But Agda-2.3.0.1 reports "no @-patterns".
Regards,
------
Sergei