Follow-up from #49, which will close #39 but uses my quick-and-dirty-but-correct MergeSort from https://github.com/dafny-lang/dafny-reportgenerator/blob/main/src/StandardLibrary.dfy#L38. That code is actually very inefficient at runtime because it relies on s[..1] slices which currently impose a full copy.

I'd personally be happy with anything based on arrays instead of sequences, but as per #39 https://en.wikipedia.org/wiki/Timsort may be an even better option.