Loop invariant for a division algorithm
A loop invariant is an expression that is true through all iterations. But it should also lead to the post-condition being true when the loop terminates. Although c-a=1 is true, It doesn't help you in achieving the post-condition.

Intuitively, You would want the invariant to be a*N + b = M because that's what division is and that's what guarantees that you'll get the post-condition ( a=quotient, b=remainder) when the termination condition ( b &lt; N ) is true. 

The formal proof should follow from this idea.