[tromp]

If the (i+1)'st outer loop starts with the first i elements in sorted order, then it ends with the first i+1 elements in sorted order.

In fact if k of the first i elements are <= A[i+1], then the first k iterations of the inner loop will not swap, and the next i-k iterations will swap. The latter can be seen to maintain order.

The last n-i iterations of the inner loop (where j>=i) do not affect this reasoning and can be omitted, as can the first iteration of the outer loop.