Dafny selection sort descending

Question

I have the following method for performing selection sort in descending order. However, the very first invariant in the while loop is said to be not maintained by the loop, why is that the case?

 method sortDesc (a : array<int>) 
        modifies a;
        requires a != null;
        ensures forall m,n :: 0 <= m < n < a.Length ==> a[m] >= a[n];
        requires a.Length > 1;
        ensures multiset(a[..]) == multiset(old(a[..]));
    {
        var index := a.Length - 1;
        while(index > -1)
            invariant forall m,n :: 0 <= m <= index && index < n < a.Length ==> a[m] >= a[n];               // all elements that we have not sorted are bigger than any element we have sorted  !!!!!!!!!!!!
            invariant a.Length > index > -1;
            invariant forall k,l :: index < k < l < a.Length ==> a[k] >= a[l];                              //the part we have gone through is already sorted!!
            invariant multiset(a[..]) == multiset(old(a[..]));                                      // USED TO MAKE SURE ALL THE STARTING ELEMENTS ARE STILL THERE!!!!!
            decreases index;
        {
            var minIndex := findMinBetween(a, index, a.Length);
            if (a[index] < a[minIndex]) 
            {
                a[index], a[minIndex] := a[minIndex],a[index];                               //SWAP ELEMENTS!!!
            }
            if (index == 0)
            {
                return;
            }
            index := index - 1;
        }
    }

Answer 1

Perhaps the comparison a[index] < a[minIndex] is the wrong way around. You are trying to move the small stuff to the right, so if a[minindex] is smaller than a[index] you need to move it (a[minindex]) to the right.