I have the following simple algorithm to find the smallest element of an array $A$ of numbers:
m = A; For i = 0 to A.length() do if m < A[i] then m = A[i]; end end return m;
The complexity of this algorithm is $O(n)$ where $n$ is the length of $A$.
I would like to prove the correctness of this algorithm using an invariant. Yet I don't know which invariant is nice here. Maybe something like: $m$ is the minimum of the subarray $A[1..k]$.