This is a much better solution than the one presented in class.

  2.2b The loop invariant: Let n = length [A]. A[j] < = A [K] 
  for all  j < =K < =  n.

Initialization: j =n
A [n] < =A [n]

Maintenance:

j = n- 1, now A'[n], the current value in the array at the nth position 
is A[n-1] if A[n] < A[n-1] and otherwise it is unchanged and in both 
cases A[n-1] < = A [n]

Assume this holds for k elements or j =n- k, 
A [n-k] < = A [L] for all L > =n-k  (1)
and show it holds for the next one which is j= n-k-1 (i.e. use induction)

We check A [n- k] < A [n-k- 1] we swap them if necessary making 
A [n-k- 1] <= A[n-k] and we know that
 A [n-k] < = A [L] for all L > =n-k, as it is our assumption. Now 
 either A [n-k- 1] = A[n-k] or A [n-k- 1] <= A[n-k] and the 
 condition (1) holds.

Termination j = i: A[i] < = A[k] for all i<= k <= n which is certainly 
true due to our maintenance step and it tells us that the smallest 
remaining element has been put into the ith place in the array.  
This is certainly a useful property.