feat: Optimize sort by MergeSort

The `MergeSort` function is in the hot path.
The slice (x[1..]) operation is not optimized in Dafny.
This optimizes this function by turning the recursive slice
into a loop over an index into the seq.
Further, a bounded integer version is also included.

It also limits the total amount of data copied.

Author: seebees