It sounds like you are willing to accept the claim that isless and isequal is more fundamental than <=. So, then your next struggle is also your solution: you must design a definition of “sequence is sorted” that relies on isless. You then notice (after a weird headache) that you can do it.
This switching of order and negation causes weird results, and the motivation is opaque to me.
I find it wrong to say that that’s the reason for the weird results. Some people are getting weird results because they are guessing incorrectly at an implementation of a function. Not only is the guess incorrect, but so would be the implementation for the default value isless.