Wrenna Robson

Just a note to say I'm an actual user and I would love this feature!

This can close once #1491 merges.

(In the end it didn't need any upstreaming - the lemma was using tons of machinery for no particular reason.)

This will require changes to Mathlib - specifically, [List.sublists_eq_sublistsFast](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/List/Sublists.html#List.sublists_eq_sublistsFast) should be removed. Embarrassingly I can't remember how to do this properly.

I am not sure about the new lemma in `‎Batteries/Data/Array/Init/Lemmas.lean`, but I cannot see where else it would be appropriate to add this lemma.

I managed to do it without needing the new lemma and now the proof is very smooth.

I'm personally in favour of Mathlib having the incomparable order as the default on Option - in some ways it's going to be quite useful to have something on it...

Yes, precisely so. And the incomparable order is the most neutral of the "obvious" choices I think. (I don't know if it should be in std4 or mathlib4. Clearly any...

Well, for the function you've given there, it seems like it "makes sense" if any input that involves none outputs false. It probably then depends how qsort is written.

(If it is written assuming totality, it should really have that as a hypothesis in some form, as a typeclass or something else.)