Hoare triple: Loop invariant and correctness
I believe the loop invariant is the same as the postcondition, except with j and m swapped with i and n, respectively. That statement can be proven true at the start and end of each loop. This is true partially by virtue of the fact that the final implication is trivially true when n = 1 (as in the outer else condition), because no k value is in the range.

The fact that j and m are only ever assigned from i and n while the invariant is true, and the postcondition is true prior to the loop, implies that the postcondition holds.

Another key observation is that i+n &lt; len implies i+n+1 ≤ len, so the proposed invariant holds true, even after the loop condition fails.

I hope that helps.