Case by ordering in linear order

Stream: Is there code for X?

[Daniel Weber]

I have three elements, x, y, z of a LinearOrder, and I want to split to the 6 cases x ≤ y ≤ z, x ≤ z ≤ y, ...
What's the nicest way to do this?

[Yaël Dillies]

obtain hxy | hyx := le_or_lt x y <;> obtain hyz | hzy := le_or_lt y z <;> obtain hzx | hxz := le_or_lt z x, then eliminate the 2 out of 8 cases that are impossible

[Daniel Weber]

What's that notation for obtain?

[Yaël Dillies]

The "I just woke up" notation :see_no_evil:

[Daniel Weber]

Ah, alright. Thanks

[Eric Wieser]

An le_total3 lemma would be reasonable in mathlib, right?

[Eric Wieser]

Alternatively, I wonder if a lemma that's says ∃ l' ∈ l.permutations, l.Sorted would be useful, then you could invoke that with [x, y, z]

[Daniel Weber]

There's docs#List.perm_mergeSort and docs#List.sorted_mergeSort, but wouldn't it be really inconvenient to use that?