On 7/8/23 19:22, Timon Gehr wrote: > `a <= b <==> a < b || b <= a` Typo. This is of course only an implication: `a <= b ==> a < b || b <= a`. In any case, the argument stands.