Loop invariant for a division algorithm I'm having problems trying to understand the concept of loop invariants.

I have the following code, where M and N are predefined constants.

a = 0
b = M
c = 1
while M - c * N &gt;= 0:
  a = c
  c = c + 1
  b = M - a * N
print(a, b)


I have figured out this code is actually a division algorithm, where in the end prints out a as the quotient of M/N and b as the remainder. But it's unclear to me what the invariant here is. Can I say c-a is the invariant since c-a=1 is always true before and after every iteration? How could I prove that in a mathematical perspective?
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.