Understanding issorted's lt keyword

Given a total order <, you can define a “less than or equal” relation <= which is:

  • a<=b if a<b or a=b

But this relation is not a total order. A sequence a_1,…,a_n is sorted if a_i<a_{i+1} or a_i=a_{i+1}, or
in other terms a_i<=a_{i+1}. The function you give to sort must be a total order, otherwise it will give
unpredictable results, so even though a function < can be used to define a function <=, you should not give <= as argument to sort (or issorted) otherwise it will misbehave.