Find an invariant in the minimum algorithm
The invariant is good (once you fix lots of imprecise things, like the 1..k which is obvious nonsense, and wouldn’t proof correctness. Precision is important. ) The code is broken, so your proof should fail - because it would be an invariant of a correct algorithm, but not your code posted here.