case splitting in linear order?

Stream: Is there code for X?

[Rémi Bottinelli]

Hey, what's the closest to a tactic that would, given variables in a linear order, create a goal for each possible ordering of the set of variables?
Ideally, something that would also take given constraint into account.
I don't believe it would be very complicated to implement? just a sequence of by_cases or trichotomy, and then close goals that have inconsistent orderings?

[Yaël Dillies]

Wait, isn't your lemma wrong? Icc a b is empty when b < a.

[Rémi Bottinelli]

That's why it's signed variation. wait